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.

Make software equivalence checker stand alone

The input

The input file format for equivalence checker is the output from Symbolic Path Finder.

testCase=test(-100,-100);pc=( !=  flags_2_SYMINT[-100] CONST_0);effects=RETURN==flags_2_SYMINT[-100];solverCalls=1;statementsExecuted=[];positionsExecuted=[];constraints=none
testCase=test(-100,-100);pc=( !=  refs_1_SYMINT[-100] CONST_0) && ( ==  flags_2_SYMINT[0] CONST_0);effects=RETURN==refs_1_SYMINT[-100];solverCalls=2;statementsExecuted=[];positionsExecuted=[];constraints=none
testCase=test(0,0);pc=( ==  refs_1_SYMINT[0] CONST_0) && ( ==  flags_2_SYMINT[0] CONST_0);effects=RETURN==10;solverCalls=2;statementsExecuted=[];positionsExecuted=[];constraints=none

The source code

Check the algorithm for the code.

After the compilation, you'll get some class files. As the code uses "jSMTLIB.jar", you also need this for execution.

Execution

This is the script with the class files.

java -cp \
.:jSMTLIB.jar:/Users/smcho/Dropbox/smcho/workspace/smcho/equivalenceChecker/bin \
EquivalenceChecker \
-r A.txt \
-t B.txt \
-m map.txt \
-e pe -s yices -p ./yices 

When you generate the executable jar, the code will be simpler.

java -cp \
.:jSMTLIB.jar \
-jar equivalenceChecker.jar \
-r A.txt \
-t B.txt \
-m map.txt \
-e pe -s yices -p ./yices 

LKT usage hint of eclipse from Use, Disuse, and Misues of Automated Refactorings paper.

Use, Disuse, and Misuse of Automated Refactorings paper has some clues on how to execute the eclipse refactoring in a programmatic way.

1. It knows the selected string - "selection-text"
2. The method that contains the selection - "code-snippet"
3. Source code - "input"
4. The kind of refactoring (maybe from the menu) - "id"

Writing a paper with LaTeX

Writing a paper accompanies bibliography, and it makes the $latex:\LaTeX$ compilation process a little more complicated.
In short, one needs to three LaTeX compilation, and one bibtex compilation.

latex refvalidator.tex
bibtex refvalidator
latex refvalidator.tex
latex refvalidator.tex # resolve all the references
dvipdfmx refvalidator.dvi

You can use \cite{} for citation, and you can have the bibliography style and bibliography for correct referencing.
You don't need \section as it will be generated automatically.

\bibliographystyle{abbrv}
\bibliography{refvalidator}