Lab 4

Implement a listener, named ArrayListener, that counts the number of reads and writes of array cells within the main method of an app. A sample run can be found below. It shows what type of output your listener should produce. Here are some hints that may be useful for implementing your listener.

• Consider the interfaces VMListener and SearchListener, which are part of the packages gov.nasa.jpf.vm and gov.nasa.jpf.search, respectively.
• Consider subclasses of the class Instruction, which is part of the package gov.nasa.jpf.vm.
• If you do not know how to count the number of reads and writes of array cells within the main method of an app, then count the number of reads and writes of array cells of the entire app.
• If you do not know how to print the total at the end, then print a star (*) every time a read or write of an array cell occurs.

To compile your listener, use

javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. ArrayListener.java

or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse.

To test your listener, you may want to use the following app.

public class ArraySample {
    public static void main(String[] args) {
        int[] array = new int[2];
        array[0] = 1;
        array[1] = array[0];
        array[0]++;
        array[1] = 2;
    }
}

To run JPF on the above app, use the following configuration file.

target=ArraySample
classpath=.
listener=ArrayListener
native_classpath=/eecs/home/franck/

where /eecs/home/franck/ is the path to the directory in which ArrayListener.class can be found.

If the above configuration file is used with the above app, JPF should produce output similar to the following.

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


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

====================================================== search started: 2/5/17 1:20 PM
*****
Total number of reads and writes of array cells: 6
*****

====================================================== 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=347,released=12,maxLive=0,gcCycles=1
instructions:       3184
max memory:         238MB
loaded code:        classes=60,methods=1320

====================================================== search finished: 2/5/17 1:20 PM

To receive feedback, submit your listener using the submit command before Monday February 5: submit 4315 lab4 ArrayListener.java