06 Apr 10 Installing and Running jpf binaries (on the command line)

In the previous post, I introduced the Java PathFinder and gave a brief overview about it and mentioned the various methods available to obtain the software on your system. In this post, I will illustrate one simple but complete cycle, right from getting the software, to installing it and then finally using it to verify a few sample Java programs. All the steps involved will be using the command line only and we will not leave the command line for the rest of this post. Also note that I have tested the steps only on my system which runs Ubuntu 9.04, but, I am pretty confident that the procedure will be the same for many other linux systems, windows or Mac Os as the jpf system is built from Java which is for the best part agnostic of the underlying operating system.

Obtaining the Binaries/Snapshots

Getting the binaries is the quickest way to get going. All you have to do is download the software, create and edit a few files and you are ready to start using jpf to verify other java programs. However, as the jpf moderators have mentioned in their website, and I quote “most JPF projects are still fast moving, so we recommend using the source repositories to stay up-to-date.”, hence we must also know how to obtain the source code and build that in order to stay abreast of the latest happenings. That, I will describe in my next post.

There are many projects listed in the site. We will concentrate only on jpf-core as of now, as it is necessary and sufficient to have it to verify some simple Java programs. The jpf-core project snapshot can be downloaded here. All you have to do is download the attachment by clicking on the link under the Attachment heading, at the bottom of the page.

Site Configurations

Now, we must take the archive that we downloaded in the previous step and unzip it in some easily accessible location. I had it unzipped in ~/binaries. Thus the complete path for the jpf-core binaries was ~/binaries/jpf-core. Next, we need to update the site.properties file which contains the information about the location. The default location of the file is ~/.jpf/site.properties. Initially, let’s just keep it that way. Hence I first created a directory and then opened the file for editing as follows,

cd ~
mkdir .jpf
emacs site.properties

For opening the site.properties file, you may use your favourite editor (gedit,vim …) instead of emacs. Now type in the following line,

# JPF site configuration
jpf-core = ~/binaries/jpf/jpf-core

It would be better to replace the ~/ sign by the complete path of your home folder and that is what I have done. Also, instead of the path I typed above, you must type the full path where you have saved the unzipped jpf-core folder. Right, now we save the above file and exit the editor.

Verification of Java programs

Finally, we get to the interesting part which is the actual verification of a sample java program. Let’s test the example program provided in the jpf website.

import java.util.Random;

public class Rand {
     public static void main (String[] args) {
          Random random = new Random(42);      // (1)

          int a = random.nextInt(2);           // (2)
          System.out.println("a=" + a);

          //... lots of code here

          int b = random.nextInt(3);           // (3)
          System.out.println("  b=" + b);

          int c = a/(b+a -2);                  // (4)
          System.out.println("    c=" + c);
     }
}

Save the above file as Rand.java at any place in your system and then execute the following statements

$javac Rand.java
$~/binaries/jpf-core/bin/jpf +classpath=.  Rand

In order to catch the error, we execute the following command

$~/binaries/jpf-core/bin/jpf +cg.enumerate_random=true +classpath=. Rand
JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center

====================================================== system under test
application: Rand.java

====================================================== search started: 7/4/10 1:29 AM
a=0
  b=0
    c=0
  b=1
    c=0
  b=2

====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
	at Rand.main(Rand.java:15)

====================================================== snapshot #1
no live threads

====================================================== results
error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty "java.lang.ArithmeticException: division by zero  a..."

====================================================== statistics
elapsed time:       0:00:00
states:             new=3, visited=2, backtracked=2, end=2
search:             maxDepth=2, constraints=0
choice generators:  thread=1, data=2
heap:               gc=4, new=302, free=44
instructions:       2893
max memory:         6MB
loaded code:        classes=70, methods=1029

====================================================== search finished: 7/4/10 1:29 AM

The java application had a divide by zero error which was caught as an ArithmeticException. For more details on the Rand.java example do refer to the original site here. You can also create your own sample java applications and test them in the manner given above. However, the next thing to focus on would be to understand exactly how the program verifies the code and what are the effective ways of testing the system.