Saturday, November 3, 2012

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. Screen Shot 2012 11 03 at 11 58 53 PM

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 

No comments:

Post a Comment