Wiki

Clone wiki

jpf-nhandler-GSoC2016 / Home

Welcome

This page contains report on work that has been done by Zhenya Tulyakov during participation in the GSoC 2016.


About the project:

JPF is the most popular model checking tool for Java applications. It is extensible and there are lots of extensions for various purposes. Jpf­nhandler is one of such extensions. Its goal is delegating the execution of SUT methods from JPF to JVM level. One goal of this project is to improve jpf-­nhandler performance using the cache layer. The latter prevents invoking methods more than once and problems caused by this. It also considerably increases the jpf­nhnandler efficiency as each method is executed only once. If jpf­nhandler encounters delegated method that has been executed, it just reflects result of its invocation. Another goal is to extend the converter component and including convertor classes for missing incompatible model classes.

Original version of the project.

Temporary version for GSoC projects.


Work schedule:

  • Integrating the delegation policy into the native peer generator (MethodPeerGen) in nhandler. (5 days including testing) ✅
  • Implementing the cache layer ✅
  • Exception handling for delegated calls (5 days) - can we make this interactive. Add an interactive mode. ✅
  • Adding more tests to cover corner cases (5 days) ✅
    • println ✅
    • Date (time does not advance if we cache the result) ✅
    • something that produces an exception depending on the input ✅
    • a native static method ✅
    • a native method that calls back to a Java method
    • other interesting/difficult cases (?) ✅
  • implementing converter objects. There should be tests for every converter. (10 days including tests)
    • java.io.FileDescriptor
    • java.io.FileOutputStream ✅
    • java.io.InputStreamReader ✅
    • java.io.OutputStreamWriter ✅
    • java.io.RandomAccessFile
    • java.lang.ClassLoader
    • java.lang.Thread
    • java.lang.ThreadLocal
    • java.lang.Throwable
    • java.lang.StackTraceElement
  • Providing a lazy update strategy ✅

The list of classes that were created/changed during within the GSoC 2016:

Created from scratch classes:

  1. nhandler.delegationPolicies.DelegationPolicy
  2. nhandler.delegationPolicies.DefaultPolicy
  3. nhandler.delegationPolicies.CachePolicy
  4. gov.nasa.jpf.vm.MapUpdater
  5. gov.nasa.jpf.vm.CacheUpdater
  6. nhandler.conversion.jpf2jvm.JPF2JVMjava_io_FileOutputStreamConverter
  7. nhandler.conversion.jpf2jvm.JPF2JVMjava_io_InputStreamReaderConverter
  8. nhandler.conversion.jpf2jvm.JPF2JVMjava_io_OutputStreamWriterConverter
  9. nhandler.conversion.jvm2jpf.JVM2JPFjava_io_FileOutputStreamConverter
  10. nhandler.conversion.jvm2jpf.JVM2JPFjava_io_InputStreamReaderConverter
  11. nhandler.conversion.jvm2jpf.JVM2JPFjava_io_OutputStreamWriterConverter
  12. delegationPolicies.CachePolicyTest
  13. delegationPolicies.JPF_delegationPolicies_CachePolicyTest
  14. CacheUpdaterTest
  15. JPF_CacheUpdaterTest
  16. MapUpdaterTest
  17. JPF_MapUpdaterTest
  18. on_the_fly.CachePolicyStringTest

Edited classes:

  1. nhandler.conversion.ConverterBase
  2. nhandler.conversion.jpf2jvm.JPF2JVMConverter
  3. nhandler.conversion.jvm2jpf.JVM2JPFjava_io_FileInputStreamConverter
  4. nhandler.peerGen.PeerMethodGen
  5. nhandler.peerGen.PeerSourceGen

And also all test classes.


Below you can find all changes with corresponding commits.

[Wed 6/1/2016]

  1. Implemented the delegation policies idea. Commits: {link1, link2, link3, link4, link5}
  2. Implemented the cache functionality. Commits: {link1, link2, link3, link4}
  3. Implemented following tests:

Additionally: fixed the bug with java_textTest.

Comparison with the proposal plan:

Today we have reached a milestone planned for June 27.

[Thu 6/9/2016]

  1. Fixed names of existing tests.
  2. Created test for native static methods.
  3. Extended CachePolicy: provided exception handling functionality.

The closest steps:

  1. Providing exception test (1-2 days).
  2. Integrating the delegation policy into the native peer generator (MethodPeerGen) in nhandler (3-5 days).

[Tue 6/14/2016]

  1. Fixed two bugs in the CachePolicy class. Commits: {link1, link2}
  2. Deleted inappropriate exception test.
  3. Integrated the delegation policy into the native peer generator (MethodPeerGen) in nhandler.

Remaining work:

  1. Testing the OTF peer generator. (June 14 - June 16).
  2. Testing the exception handling (June 17).
  3. Testing native methods that depend on object data (June 18 - June 19).
  4. Implementing listeners for cached objects [?] (June 20 - June 23).
  5. Implementing converter objects. (June 24 - July 10).
  6. Integrating the conformance checker tool into nhandler. (July 10 - July 15).
  7. Providing a lazy update strategy (July 15 - July 30).

[Thu 6/16/2016]

  1. Fixed a bug with null-member`s hashcode in the CachePolicy class.
  2. Created tests for both DefaultPolicy and CachePolicy functionality int OTF peers.

Remaining work:

  1. Testing the exception handling (June 17).
  2. Testing native methods that depend on object data (June 18 - June 19).
  3. Implementing converter objects. (June 20 - July 10).
  4. Integrating the conformance checker tool into nhandler. (July 10 - July 15).
  5. Providing a lazy update strategy (July 15 - July 30).

[Tue 6/20/2016]

  1. Fixed a bug in the CachePolicy class: resolved a problem with exception names.
  2. Provided a test for exception handling functionality.
  3. Deleted unused imports in the classes of the tests.delegationPolicies.
  4. Fixed CachePolicy class: deleted nullity check for methods; -2147483648 is replaced with Integer.MIN_VALUE.

Remaining work:

  1. Investigating converters. (June 21 - June 25)
  2. Implementing converter objects. (June 25 - July 10).
  3. Integrating the conformance checker tool into nhandler. (July 10 - July 15).
  4. Providing a lazy update strategy (July 15 - July 30).

[Tue 6/27/2016]

  1. Created test that checks whether CachePolicy returns same object during multiple calls.
  2. Created test that demonstrates a drawback caused by abscence of listeners.
  3. Deleted unused imports in delegation policies and their tests.

Remaining work:

  1. Investigating converters. (June 27 - July 1).
  2. Implementing converter objects. (July 1 - July 15).
  3. Integrating the conformance checker tool into nhandler. (July 15 - July 20).
  4. Providing a lazy update strategy (July 20 - August 5).
  5. Implementing listeners for cached objects (August 5 - August 8).

[Fri 7/8/2016]

  1. Created both JPF2JVM and JVM2JPF converters for java.io.FileOutputStream.
  2. Created tests for both JPF2JVM and JVM2JPF converters for such classes:
    • java.io.FileInputStream
    • java.io.FileOutputStream

Remaining work:

  1. Implementing JPF2JVM and JVM2JPF converters and tests for such classes:
    • java.io.InputStreamReader (July 9 - July 10)
    • java.io.OutputStreamWriter (July 11 - July 12)
    • java.io.RandomAccessFile (July 13 - July 14)
  2. Providing a lazy update strategy (July 14 - July 25).
  3. Implementing listeners for cached objects (July 25 - August 1).
  4. Integrating the conformance checker tool into nhandler. (August 31 - August 3).

[Sun 7/17/2016]

  1. Created both JPF2JVM and JVM2JPF converters for java.io.InputStreamReader.
  2. Created both JPF2JVM and JVM2JPF converters for java.io.OutputStreamWriter.
  3. Created tests for these converters.
  4. Fixed JVM2JPF converters for java.io.FileInputStream and java.io.FileOutputStream: fixed a problem with restoration of JPF files.

Both java.io.FileInputStream and java.io.FileOutputStream contain an instance of java.io.FileDescriptor. Jpf-nhandler does not have a converter for this class and generic converter is not appropriate as there is a mismatch between java standard class and JPF model class. So instance of FileDescriptor is created in the converters for FileOutputStream and FileInputStream. JPF model class for FileDescriptor contains a field of type String called "fileName". It is responsible for restoration of the FileDescriptor. Basically it was set to MJIEnv.NULL as there was not an opportunity to instantiate it correctly. However, in some cases we can retrieve this field from "path" field in the FileInputStream and FileOutputStream. And this is what was implemented by me.

  1. Changed tests for java.io.FileInputStream and java.io.FileOutputStream respectively.

Remaining work:

  1. Providing a lazy update strategy (July 18 - August 1).
  2. Implementing listeners for cached objects (August 1 - August 10).

[Mon 7/25/2016]

  1. Created a listener that notifies updates of the objects that have been converted from JPF to JVM and stored in the map. Commits: {link1, link2, link3}

Remaining work:

  1. Testing and refining a MapUpdater (July 25 - August 1).
  2. Implementing listeners for cached objects (August 1 - August 10).

NOTE: the timeline is approximate

[Fri 7/28/2016]

  1. Fixed the MapUpdater functionality.
  2. Created test for the MapUpdater.

Remaining work:

  1. Implementing method in the MapUpdater that notifies changes in arrays. Creating a test. (July 29 - August 1).
  2. Implementing listeners for cached objects (August 2 - August 10).

NOTE: the timeline is approximate

[Sun 7/31/2016]

  1. Extended functionality of the MapUpdater: added the code that listens for changes of the fields of arrays and updates an array whose field was changed.
  2. Created a test that checks a functionality of updating of arrays by the MapUpdater.

Remaining work:

  1. Removing parts of the code that clears a map that contains converted from JPF 2 JVM objects in the ConverterBase. (August 1)
  2. Implementing listeners for cached objects (August 2 - August 10).

[Wed 8/3/2016]

  1. Extended functionality of the MapUpdater:
    • added the code that resets ConverterBase after the SUT execution.
    • changed the part of code that updates the JPF2JVM map in case when a stored object was changed: now the MapUpdater just removes the object from the map instead of updating it. Actual approach is preferable to previous as it allows avoid redundant expenses of the time and the memory.
  2. ConverterBase.reset(MJIEnv env) is divided into two methods:
    • ConverterBase.resetJVM2JPF() - invoked at the beginning of the each peer methods created on-the-fly and at the end of the SUT execution;
    • ConverterBase.resetJVM2JPF() - invoked at the end of the SUT execution;
  3. Changed peer methods of the tests in accordance with aforementioned change.
  4. Changed PeerMethodGen and PeerSourceGen classes according to the change of the ConverterBase.reset(MJIEnv env).

Remaining work:

  1. Implementing a listener for cached objects (August 4 - August 14).

[Mon 8/8/2016]

  1. Changed a delegateCall() method`s declaration of the DelegationPolicy class:
    • Got rid of the MJIEnv env parameter - it can be reached from any piece of code, so giving it as a parameter is redundant;
    • Added new arg - int[] indexes - JPF indexes of the objects-args of the delegated method, including the object/class that called this method.
  2. Changed bodies of the native peers of tests that delegate methods using DelegationPolicy`s subclasses. The changes are caused by the changed signature of the delegateCall() method.
  3. Changed parts that generate bodies of native peer methods (PeerMethodGen and PeerSourceGen) according to changes in the DelegationPolicy.delegateCall method: added creating and instantiating of the array that contains JPF indexes of the arguments of delegated method.
  4. Created a listener for the CachePolicy class - the CacheUpdater. If any object that comprises an argument list of the method was changed on the JPF side, the CacheUpdater removes the entire entry that contains a method, a callee of the method, arguments to the method and returned value from the cache storage.
  5. Provided tests for the functionality of the CacheUpdater.

Remaining work:

Refining the CacheUpdater.

[Wed 8/10/2016]

  1. Extended functionality of the CachePolicy:
    • Added a map called flagStorage that contains information about results of execution of different methods;
    • Extended functionality of the delegateCall method - now it adds information about the method execution into the flagStorage;
    • Extended functionality of the removeIfPresent method - now it updates both storage and exceptionStorage in the case when arguments of a certain method or its callee was changed.
  2. Created additional tests for the CacheUpdater.

[Fri 8/12/2016]

  1. Fixed a line of code of the PeerSourceGen that generates a code for delegation of a method: argument MJIEnv env is replaced with int[] argIndexes.
  2. Changed JVM2JPFConverter: added methods that updates JVM objects in the ConverterBase.objMapJPF2JVM and JVM classes in the ConverterBase.classMapJPF2JVM in accordance with given JPF objects/classes.
  3. Changed ConverterBase class: added a method called updateIfPresent that updates a JVM object/class if it is present in the objMapJPF2JVM/classMapJPF2JVM.
  4. Got rid of redundant tests in CacheUpdaterTest and MapUpdaterTest.
  5. Added test in "JVM2JPFTest for updating of reference arrays functionality. Added here because temporarily cannot be verified using the MapUpdater*.
  6. Updated the CacheUpdater: deprecated calls of the method ElementInfo.getInstance() is replaced with ElementInfo.getObjectRef.
  7. Changed MapUpdater: deleted redundant piece of code that updates non-reference arrays.

[Tue 8/16/2016]

  1. Extended MapUpdater: added method that resets ConverterBase after backtracking.
  2. Extended CacheUpdater: added method that resets the CachePolicy after backtracking.

NOTE: the timeline is approximate


Map updating mechanism.

As we know, jpf-nhandler uses a map to store objects/class converted from JPF to JVM. JPF2JVMConverter that translates objects from JPF to JVM firstly check whether certain object/calss is stored in the map. If yes, it returns those object/class and create new otherwise. Previously this map needed to be cleared at the beginning of each method created on-the-fly because the JPF object/class could be changed and not updated JVM object/class was not correct. Therefore, it was not relible to use converted object/class stored in the map. That`s why user could specify whether or not to clear the map at the beginning of the method, configuring property "nhandler.resetVMState". Actually the map gets updated and there is no need to clear it. The map updating mechansim is implemented using listener called "MapUpdater". It listens for instructions 'PUTFIELD', 'PUTSTATIC' and 'AASTORE' then gets a JPF index of the changed object/class and then calls a method of the ConverterBaseClass named "updateIfPresent(int JPFRef)". This method checks if either map that stores objects or the one that stores classes contains object/class and update those object/class using methods "updateJVMClass" or "updateJVMObj" of the JPF2JVMConverter. These methods choose proper converter for the class/object and then just set instance or static fields of the object/class. This allows us avoid recreating objects and prevents from problems caused by it.

The drawback connected with updating of reference arrays

There is no need to update non-reference arrays as they get updated automatically, that`s why MapUpdater needs to update only reference arrays. To achieve this, it listens for instruction called 'AASTORE'. If it is called, MapUpdater gets a JPF reference of the array using method "getArrayReference(ThreadInfo currentThread)" and it always returns "0". This bug is not related to jpf-nhandler but does allow MapUpdater to update reference arrays. This issue needs to be explored and addressed.


Features that should be implemented in future.

  1. Resolving a problem connected with reference arrays. Neither CacheUpdater nor MapUpdater can perform properly: both of them needs a JPF index of reference arrays to update CachePolicy/ConverterBase clases. They should be retrieved from an AASTORE instance using method "getArrRef(ThreadInfo currentThread)". However, in both cases it returns "0" - i.e. null-value. It needs to be deeper explored and fixed.

  2. Adding JPF2JVM and JVM2JPF converters for different classes, such as: java.io.FileDescriptor etc. Jpf-nhandler uses converters to translate classes from JPF to JVM and vice verca. If there is one-to-one correspondence between original Java class and JPF model class, the GenericConverter is used. If such strict equality is not held, jpf-nhandler needs specific converters for proper instantiation of the object`s fields. There are still some classes that do not have implemented converters.

  3. Adding automatic ConformanceChecker. Jpf-nhandler uses instances of the ConformanceChecker class to decide either to use GenericConverter for object translation or specific converter. Current approach uses manually initialized array that contains names of classes that need specific converters. The idea is to implement a checker that will compare fields of Java class and correspondant JPF model class and check whether or not there is any mismatch between them.

Updated