Making Symbolic Path Finder standalone

Setup

In order to use JPF/SPF, one needs a setup file in "~/.jpf/site.properties" file. This setup file is a pointer that points where all the core files and extensions are located.

# JPF site configuration
user.home = DIRECTORY
jpf.home = ${user.home}/DIR1
jpf.libraries = DIR2

# can only expand system properties
jpf-core = ${jpf.libraries}/jpf-core

jpf-symbc = ${jpf.libraries}/jpf-symbc
extensions+=,${jpf-symbc}

The pointed directory has another "jpf.proterites" configuration files. Inside the file, we have all the directory information that points to the jar file and others.

...

jpf-core = ${config_path}

jpf-core.native_classpath=\
  ${jpf-core}/build/jpf.jar;\
  ${jpf-core}/build/jpf-annotations.jar;\
  ${jpf-core}/lib/junit-4.10.jar

jpf-core.classpath=\
  ${jpf-core}/build/jpf-classes.jar;\
  ${jpf-core}/build/examples

jpf-core.sourcepath=\
  ${jpf-core}/src/examples

jpf-core.test_classpath=\
  ${jpf-core}/build/tests

jpf-core.peer_packages = gov.nasa.jpf.jvm,,

...

Java code with package

This is the sample code.

package a.b;

public class HelloA {
	public int testRefactored (int refs, int flags) {
	    if (flags != 0) 
	    	return flags;
	    else if (refs != 0)
	    	return refs;
	    return 10;       
	  }
	
	public static void main(String[] args) {
		HelloA ex = new HelloA();
		int ret = ex.testRefactored(0,0);
		System.out.print(ret);
	}
}

We need to compile this java code using debug flag "-g", and move the generated class file where the java can find it.

javac -g HelloA.java
mkdir -p a/b

Then, we need the setup file. In this setup file, one needs to specify the listener. In this listener example, it specifies the listener class, and it should be located in somewhere where the "site.properties" can point to.

target = a.b.HelloA

basedir = PATH
rse.testFile = ${basedir}/HelloA.txt
symbolic.method= a.b.HelloA.testRefactored(sym#sym)
rse.testCases = true

listener = gov.nasa.jpf.porting.listener.RSESymbolicListener

#If we don't set the bounds then one of the constraints times out.
symbolic.min_int=-100
symbolic.max_int=100
symbolic.min_double=-1000.0
symbolic.max_double=1000.0
symbolic.undefined=0

Then we can execute the JPF jar binary.

JPF_JAR_DIR=/Users/smcho/Dropbox/smcho/research/jpf/jpf-core/build
java -jar ${JPF_JAR_DIR}/RunJPF.jar ./HelloA.jpf 

This is an example to get two summary files to execute the software equivalence checker.

mkdir -p a/b
#
javac -g HelloA.java
mv HelloA.class a/b
#
JPF_JAR_DIR=/Users/smcho/Dropbox/smcho/research/jpf/jpf-core/build
java -jar ${JPF_JAR_DIR}/RunJPF.jar HelloA.jpf
#
mkdir -p c/d
#
javac -g HelloB.java
mv HelloB.class c/d

JPF_JAR_DIR=/Users/smcho/Dropbox/smcho/research/jpf/jpf-core/build
java -jar ${JPF_JAR_DIR}/RunJPF.jar HelloB.jpf

Java code with no package

With the java source without package, everything is the same except

• No need to move the class file into the directory.
• No need to prepend the package info in the configuration files.