Midnight Researcher Notes: Getting Started with Java PathFinder

Java™ Pathfinder, or "JPF" as we call it from here, is a highly customizable execution environment for verification of Java™ bytecode programs. JPF was developed at the NASA Ames Research Center, open sourced in 2005, and is freely available here under the NOSA 1.3 license. JPF started as a software model checker but it integrates model checking, program analysis and testing.

In this post we will go in a step by step process to setup the environment where Java Path Finder can be used within Eclipse IDE environment. We will show a simple example of using JPF.

Step 1. Install Eclipse
- Step 1.1 : Download and install the latest JDK fro your platform from here.
- Step 1.2 : Download the latest Eclipse from here. Once you have unzipped the previously downloaded file, you will see a folder named eclipse. In that folder you will find the eclipse application. We recommend you create a shortcut on the desktop to simplify the launching of eclipse. Notice that unlike Java, Eclipse does not have an installation process. Once you have unzipped the file you are done.
Step 2. Download JPF

Step 2.1 : Download Mercurial plug-in for Eclipse
- Launch Eclipse. Go to Help >> Install New Software
- Click Add
- Insert “Mercurial” in the Name box. Insert “http://mercurialeclipse.eclipselabs.org.codespot.com/hg.wiki/update_site/stable/” in the Address box. Click Ok.
- In the install dialog select the newly added site from Work with drop down box. The list below it will show the available software at this site, select the item named MercurialEclipse and click Next, then finish..
Step 2.2 : Download the JPF source code
- In Eclipse menu : File >> Import >> Mercurial >> Clone Existing Mercurial Repository >> Next.
- In the repository location URL, insert “http://babelfish.arc.nasa.gov/hg/jpf/jpf-core”. Click Next, then Finish. The JPF project files will be downloaded to your local computer.
Step 2.3 : Build the JPF

In the package explorer, select the build.xml, right click on it, select “run as” >> “Run as Ant build “.
Eclipse will build JPF and a new folder named “build” will appear in the package explorer (it may not appear even the build was successful, double check the windows explorer for it.)

If the build failed due to error missing JDK:

On Eclipse menu : Project >> Properties. Select Builders from the lift hand side list
Select Ant Builder and click New.
Select Ant Builder and click New.
In the Edit Configuration dialog, select the “JRE” tab, then select “Separate JRE” from the “Runtime JRE section”. In the drop down list, select JDK:
If you couldn’t find the JDK in the drop down list, click “Installed JRE …”
In the “Preferences” dialog, click “Add”
Select “Standard VM” and click “Next”
Click “Directory” and navigate to your JDK installation directory. Then click “Finish” to return to the previous dialog.
Select the JDK and click Ok.
Select JDK in the drop down box and click OK

Step 3 : Install and configure JPF
- Step 3.1 : Install JPF files : Copy the whole jpf-core project folder into <user.home>/projects/jpf
- Step 3.2 : Create site.properties
  - Create site.properties under <user.home>/.jpf folder.
  - To create the folder on windows, use the following command on the command window after navigating to the user home: mkdir .jpf .
  - Paste the following content into the site.properties file.
```
# JPF site configuration

jpf.home = ${user.home}/projects/jpf

# can only expand system properties
jpf-core = ${user.home}/projects/jpf/jpf-core

# annotation properties extension
jpf-aprop = ${jpf.home}/jpf-aprop
extensions+=,${jpf-aprop}
# numeric extension
jpf-numeric = ${jpf.home}/jpf-numeric
extensions+=,${jpf-numeric}
# concurrent extension
#jpf-concurrent = ${jpf.home}/jpf-concurrent
#extensions+=,${jpf-concurrent}
jpf-shell = ${jpf.home}/jpf-shell
extensions+=,${jpf-shell}
jpf-awt = ${jpf.home}/jpf-awt
extensions+=,${jpf-awt}

jpf-awt-shell = ${jpf.home}/jpf-awt-shell
extensions+=,${jpf-awt-shell}
```
- Step 3.3 : Install Eclipse plug-in
  - The JPF Eclipse plug-in allows you to invoke JPF directly from Eclipse.
  - In Eclipse go to Help >> Install New Software.
  - In the new window click Add. In the name insert JPF. In the location insert “http://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/install/eclipse-plugin/update/” then click Ok.
  - From the “Work with:” drop down menu select the newly added site.
  - In the list, check “Eclipse-JPF”, click Next, then Finish.
Step 4 : Start the demo project
- Step 4.1 : Create and configure project
  - In Eclipse menu : File >> New >> Java project : project name = jpf_junit_demo
  - In the package explorer, right click on the project name. Choose “Build Path” >> “Add libraries”
  - Select User Library and click Next.
  - Click User libraries. Then New. You will see a window for creating a library. Put “jpf” as the library name and click Ok to return to the previous dialog.
  - Select the newly added jpf library and click “Add External JARs …”.
  - Select all the jar files under <user.home>/jpf/jpf-core/build and click “Open” to add them under library jpf
  - Click New to create a new user library. Name it “jpf-support”.
  - Select the newly added jpf-support library and click “Add External JARs …”.
  - Select all the jar files under <user.home>/jpf/jpf-core/lib and click “Open” to add them under library jpf-support
  - Now the User Libraries should look like the following:
  - Right click on the project name and select : New >> Folder, name the folder as test. Right click on the newly created test folder and select : Build Path >> Use as Source Folder. This folder will be used in the future to hold the JUnit test classes.
  - Now the project folder should look like the following:
- Step 4.2 : Create a class (program under test)
  - Right click on the “src” folder and choose: New >> Class. Name it Calculator and click Finish.
  - This is the content of the very simple Calculator.java which prints the sum of two integers. The Verify statements are the only JPF statements, the rest is pure java. We will explain the JPF statements through its results in the next step.
```
import gov.nasa.jpf.jvm.Verify;

public class Calculator {
    int add (int a, int b)
    {
        return a+b;
    }
    public static void main(String[] args)
    {
        int a = Verify.getInt(1,3);
        int b = Verify.getInt(5,8);
        Calculator cal = new Calculator();
        System.out.println(a + "+" + b + "=" + cal.add(a, b));
    }
}
```
  - Step 4.3 : Run JPF from Eclipse
    - Right click on the project name and select: New >> File. Name the file “jpf_junit_demo.jpf”.
    - This is the content of the newly added file
      +classpath=${config_path}/bin
      target=TestGenerator
    - In the package explorer, right click on the “jpf_junit_demo.jpf” and select “Verify …”.
    - If you couldn’t see the “Verify…” option, this means that you didn’t installed the JPF plug-in properly. See step 3.3.
    - JPF will get started and you will see its output in the console pane. It will be like the following:
```
Executing command: java -jar C:\Users\Ebeid\projects\jpf\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Ebeid\projects\jpf_junit_demo\jpf_junit.demo.jpf
JavaPathfinder v6.0 (rev 960+) - (C) RIACS/NASA Ames Research Center

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

====================================================== search started: 3/28/13 4:41 PM
1+5=6
1+6=7
1+7=8
1+8=9
2+5=7
2+6=8
2+7=9
2+8=10
3+5=8
3+6=9
3+7=10
3+8=11

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:02
states:             new=5, visited=11, backtracked=16, end=12
search:             maxDepth=3, constraints hit=0
choice generators:  thread=1 (signal=0, lock=1, shared ref=0), data=4
heap:               new=545, released=197, max live=353, gc-cycles=13
instructions:       5098
max memory:         55MB
loaded code:        classes=82, methods=1362

====================================================== search finished: 3/28/13 4:41 PM
```
  According to our program code and the JPF results, you may already guessed what the verify statements are doing in the following lines of code:
  
  int a = Verify.getInt(1,3);
  int b = Verify.getInt(5,8);
  - Simply, Verify.getInt(x, y) get a new integer within the range [x,y].
  - That is it ?
  - Partially yes.
  - But how JPF get 12 print outputs ?
  - Ok Actually JPF starts a new clone of the program for each value resulted from a Verify.getInt() statement.
  - This means that JPF will create 3 versions of the program, each one of these versions runs with a different value of a (1, 2, 3).
  - Each version of these three versions will be used as a base to create another 4 versions of the program for variable b, each one of these versions runs with a different value of b (5, 6, 7, 8).
  So, the total versions of the program running by JPF is 3 * 4 = 12. Its like a tree where the leafs are the print statements :
  - a = 1
    - a = 1, b = 5 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 1+5=6
    - a = 1, b = 6 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 1+6=7
    - a = 1, b = 7 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 1+7=8
    - a = 1, b = 8 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 1+8=9
  - a = 2
    - a = 1, b = 5 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 2+5=7
    - a = 1, b = 6 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 2+6=8
    - a = 1, b = 7 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 2+7=9
    - a = 1, b = 8 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 2+8=10
  - a = 3
    - a = 1, b = 5 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 3+5=8
    - a = 1, b = 6 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 3+6=9
    - a = 1, b = 7 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 3+7=10
    - a = 1, b = 8 | System.out.println(a + "+" + b + "=" + cal.add(a, b)); | 3+8=11
  you can use JPF for your JUnit tests to generate explore your code states as we did; just keep in mind that a small increase in the number of states of variables could result in huge number of total program states.
  
  I hope you enjoyed it, and see you later in more posts about JPF.

Saturday, March 30, 2013

Getting Started with Java PathFinder