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