Saturday, November 3, 2012

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. Screen Shot 2012 11 03 at 11 32 06 PM 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 
Screen Shot 2012 11 03 at 11 52 14 PM 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. 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 

XML parsing/generation with ElementTree

Parsing XML

Let's say we want to parse this XML code.
  • The XML has the root element of "data".
  • Inside the root element, we have "TestA".
  • Inside the "TestA" element, we have multiple "Source" elements.
  • The "Source" element has three attributes.

 
  
 

Maybe the most convenient way to parse this XML is using ElementTree with Python. You can get the root with getroot() method.
import xml.etree.ElementTree as ET

tree = ET.parse('setup.xml')
root = tree.getroot()
From the root (or any element object), you can get the element with find() method with the element name as parameter. You can get the element whatever you want likewise.

The interesting thing you notice is that the element object returns iterator that gives all the sub elements.

The element object also has the attrib dictionary that contains the attributes.
testA = root.find('TestA')
sources = testA.find('Source')

for source in testA: # testA returns all the sub elements. 
    print source.attrib
    print source.attrib['numberOfParams']
    print source.attrib['filePath']
    print source.attrib['method']
This is the result to run the script.
{'numberOfParams': '2', 'method': 'method', 'filePath': 'Charlie'}
2
Charlie
method

Generating XML

You can crete the Element object with Element() with name of the element as a parameter.
root = ET.Element('data')
With SubElement with first parameter as the element object, and the second as the element name, one can add sub elements. As element object has the attrib dictionary, by filling in the dictionary one can add attributes.
testChoice = ET.SubElement(root, 'TestA')
source = ET.SubElement(testChoice, 'Source')
source.attrib[key] = sourceInfo[key]
And to string method generates string, and you can just save the string into a file.
xml_str = ET.tostring(root)
with open("./hello.xml","w")  as f:
            f.write(xml_str)
For element object you can use the dump() method
ET.dump(root)
The code to generate the xml can be as follows:
import xml.etree.ElementTree as ET
import re

class Source:
    def __init__(self):
        self.method = "method"
        self.filePath = "filePath"
        self.numberOfParams = 2
        
    def buildSource(self, data, testChoice, **sourceInfo):
        testChoice = ET.SubElement(data, testChoice)
        source = ET.SubElement(testChoice, 'Source')
        for key in sourceInfo.keys():
            print key, sourceInfo[key]
            source.attrib[key] = sourceInfo[key]
        
    def buildXml(self):
        root = ET.Element('data')
        sourceInfo = {}
        sourceInfo['filePath'] = "Charlie"
        sourceInfo['numberOfParams'] = "%d" % 2
        sourceInfo['method'] = "method"
        self.buildSource(root, 'TestA', **sourceInfo)
        
        xml_str = ET.tostring(root)
        
        #root = ET.fromstring(xml_str)
        ET.dump(root)
        with open("./hello.xml","w")  as f:
            f.write(xml_str)

source = Source()
source.buildXml()