Part of my Google Summer of Code project this summer involved building a visualization tool to help examine trace files used by JPF Guided Test and a related under-approximation scheduler. The visualization tool is in the Guided Test repository. I was using Eclipse to manage the project. Everything built correctly but the program didn’t work because the icons were not in the build folder as expected. A quick hint from stackoverflow was that the solution is to use Ant.
<target name="-pre-jar" description="Copy Images">
<property name="images.dir" value="build/main/edu/byu/cs/guided/search/visualize/graphics" />
<copy todir="${images.dir}">
<fileset dir="./src/main/edu/byu/cs/guided/search/visualize/graphics" />
</copy>
<echo level="info" message="Visualization icons was copied."/>
</target>
The key is to use the “-pre-jar” target in the build.xml file to copy the files into the right spot. This change was part of the visualization check-in into the repository. Some documentation on Ant targets is available in the Apache Ant User Manual. This StackOverflow entry on adding resource files to a jar file with Ant has some useful hints as well.
The NASA AMES site has the necessary documentation for this procedure (and all else JPF). Nonetheless, I’m documenting the process here to save me some time the next time I need to do this since all commands will be in one spot.
For this project, I was running a Windows 7 box but these instructions should be easy to port to Linux other platforms. You will need to install the latest version of the Java Runtime Environment (JRE) and the Java Development Kit (JDK). Without the JDK installed (and included in your PATH environment variable), you will get the famous “javac is not recognized as an internal or external command.” These tools can be found on Sun’s website. Proceed to the command line and verify that these commands list the most up to date recent Java version available (JDK 6 Update 20 as of this posting).
javac -version
java -version
You will also need Mercurial to install JPF. For windows users, it may be easier to install TortoiseHg since it will automatically add the hg command to the PATH [needs confirmation]. On my system, I installed the JPF core into a JPF folder I created in my home folder. To do so, drop to the command line then:
cd %HOMEPATH%
mkdir jpf
cd jpf
hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core
To build the source and run the test suite:
cd jpf-core
bin/ant test
This ant script requires the JAVA_HOME environment variable to be set (on Windows anyway). I set it to my JDK installation path.
Note: for my initial checkout, I cloned http://babelfish.arc.nasa.gov/hg/jpf but expecting to get the whole tree, but the subrepositories were empty! All the extensions must be separately cloned. Before running the Racer example mentioned on the JPF page, you need to set up the site.properties file. This file should be placed in a folder called “.jpf” in the user’s home directory. Attempting to run the example before setting up this file will give you the error message: “gov.nasa.jpf.JPFClassLoaderException: no classpath entry for gov.nasa.jpf.JPF found (check site.properties)”.
cd %HOMEPATH%
mkdir .jpf
cd .jpf
echo # JPF site configuration > site.properties
echo # >> site.properties
echo jpf-core = ${user.home}/jpf/jpf-core >> site.properties
echo # >> site.properties
echo # numeric extension >> site.properties
echo jpf-numeric = ${user.home}/jpf/jpf-numeric >> site.properties
echo extensions+=${jpf-numeric} >> site.properties
echo # >> site.properties
echo # annotation-based program properties extension >> site.properties
echo jpf-aprop = ${user.home}/jpf/jpf-aprop >> site.properties
echo extensions+=,${jpf-aprop} >> site.properties
echo # >> site.properties
echo #... and all your other installed projects >> site.properties
echo # >> site.properties
Verify that site.properties has been successfully created. Now we can run the example:
java -jar build/RunJPF.jar src/examples/Racer.jpf
Et voila! You should now see output like:
JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center
====================================================== system under test
application: Racer.java
====================================================== search started: 7/1/10 5:51 PM
10
10
====================================================== error #1
gov.nasa.jpf.listener.PreciseRaceDetector
race for: "int Racer.d"
main at Racer.main(Racer.java:16)
"int c = 420 / racer.d; // (4)" : getfield
Thread-0 at Racer.run(Racer.java:7)
"d = 0; // (2)" : putfield
====================================================== snapshot #1
thread index=0,name=main,status=RUNNING,this=java.lang.Thread@0,target=null,priority=5,lockCount=0,suspendCount=0
call stack:
at Racer.main(Racer.java:16)
thread index=1,name=Thread-0,status=RUNNING,this=java.lang.Thread@272,target=Racer@271,priority=5,lockCount=0,suspendCount=0
call stack:
at Racer.run(Racer.java:7)
====================================================== results
error #1: gov.nasa.jpf.listener.PreciseRaceDetector "race for: "int Racer.d" main at Racer.main(Race..."
====================================================== statistics
elapsed time: 0:00:00
states: new=9, visited=1, backtracked=4, end=2
search: maxDepth=5, constraints=0
choice generators: thread=8, data=0
heap: gc=8, new=278, free=32
instructions: 2956
max memory: 15MB
loaded code: classes=68, methods=988
====================================================== search finished: 7/1/10 5:51 PM