JPF summary generation test1

Simple Example

A.java

public int sub(int a, int b)
{
    return a - b;
}
public int testRefactored (int refs, int flags) {
    if (flags != 0) 
    	return flags * sub(flags, flags*3);
    else if (refs != 0)
    	return refs;
    return 10;       
}

(or ( and  (distinct  flags_2_SYMINT 0)  (=  RETURN ( * (flags_2_SYMINT- (flags_2_SYMINT * 3)) flags_2_SYMINT)) )
 ( and  (distinct  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN refs_1_SYMINT) )
 ( and  (=  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN 10) )
)

JPF is smart enough to understand sub() method to give the correct constraints

RETURN ( * (flags_2_SYMINT- (flags_2_SYMINT * 3)

B.java

public int sub(int a, int b)
{
    return a - b;
}
public int testRefactored (int refs, int flags) {
    if (flags != 0) 
    	return flags;
    else if (refs != 0)
    	return refs;
    return 10;       
}

(or ( and  (distinct  flags_2_SYMINT 0)  (=  RETURN flags_2_SYMINT) )
 ( and  (distinct  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN refs_1_SYMINT) )
 ( and  (=  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN 10) )
)

More complex

With this example:

public int sub(int a, int b)
{   
	if (a > b)
		return (a - b);
	else
	    return (10*a + b);
}
public int test (int refs, int flags) {		
	if (flags != 0) 
		return flags * sub(flags, flags*3); << This line causes an issue
	else if (refs != 0)
	   	return refs;
	return 10;       
}

JPF works fine to generate the correct summary:

testCase=test(-100,-100);pc=( >  flags_2_SYMINT[-100] ( *  flags_2_SYMINT[-100] CONST_3)) && ( !=  flags_2_SYMINT[-100] CONST_0);effects=RETURN==( *  (flags_2_SYMINT[-100] - (flags_2_SYMINT[-100] * CONST_3)) flags_2_SYMINT[-100]);solverCalls=2;statementsExecuted=[];positionsExecuted=[];constraints=none
testCase=test(1,1);pc=( <=  flags_2_SYMINT[1] ( *  flags_2_SYMINT[1] CONST_3)) && ( !=  flags_2_SYMINT[1] CONST_0);effects=RETURN==( *  ((flags_2_SYMINT[1] * CONST_3) + (flags_2_SYMINT[1] * CONST_10)) flags_2_SYMINT[1]);solverCalls=2;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

Only to get something's wrong with the listener:

(or  ( and  (>  flags_2_SYMINT ( * flags_2_SYMINT 3))  (distinct  flags_2_SYMINT 0)   (=  RETURN ( * (flags_2_SYMINT- (flags_2_SYMINT * 3)) flags_2_SYMINT)) )
 ( and  (<=  flags_2_SYMINT ( * flags_2_SYMINT 3))  (distinct  flags_2_SYMINT 0)   (=  RETURN ( * ((flags_2_SYMINT * 3)+ (flags_2_SYMINT * 10)) flags_2_SYMINT)) )
 ( and  (distinct  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN refs_1_SYMINT) )
 ( and  (=  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN 10) )
)
 ( and  (<=  flags_2_SYMINT ( * flags_2_SYMINT 3))  (distinct  flags_2_SYMINT 0)   (=  RETURN ( * ((flags_2_SYMINT * 3)+ (flags_2_SYMINT * 10)) flags_...
                                                                                                    ^^^^^^^^^^^^^^
(error "Invalid beginning of an identifer: expected either 'as' or '_' here")
Executing the script...
 ( and  (<=  flags_2_SYMINT ( * flags_2_SYMINT 3))  (distinct  flags_2_SYMINT 0)   (=  RETURN ( * ((flags_2_SYMINT * 3)+ (flags_2_SYMINT * 10)) flags_...
                                                                                                    ^^^^^^^^^^^^^^
(error "Invalid beginning of an identifer: expected either 'as' or '_' here")

sub(flags, flags*3)

I think the generated code should have been (* flags_2_SYMINT 3).

Research questions

• How does the listener work to transform summary into S-expression code
• How do I modify the listener to resolve this issue?

Tracing into LTK refactoring library

I needed to trace into eclipse refactoring library, and I could do that by installing eclipse source code.

Lars Vogel's Eclipse Source Code gives very simple and effective way of installing eclipse source.

How to get file path information from ICompilationUnit?

When you have ICompilationUnit, you can get the java file path for the unit using this code.

IResource resource = iCompilationUnit.getUnderlyingResource();
if (resource.getType() == IResource.FILE) {
    IFile ifile = (IFile) resource;
    String path = ifile.getRawLocation().toString();
}

References

• How to get file path information from ICompilationUnit?

Writing file from CompilationUnit (ASTNode)

When you have an object of iCompilationUnit, you can save it to the file.

1. You need to create Document object from ICompilationUnit
2. You need a ASTRewrite object from CompilationUnit
3. Filling in the Document object using apply() method
4. Storing the source code string from document.get() method

Document document = new Document(iCompilationUnit.getSource());
ASTRewrite rewriter = ASTRewrite.create(compilationUnit); // ? check if the parameter object type is correct

rewrite.rewriteAST().apply(document);
String source = document.get();

File file = new File(DEST_FILE_PATH);
FileUtils.writeStringToFile(file, source) 

FileUtils

You need to save apache file utilities to use the FileUtils.

References

• Saving modified AST in a new file with eclipse plugin
• Using FileUtils in eclipse

How you can get CompilationUnit (AST) from Workspace in eclipse?

The starting point is to get WorkSpace, and you can do that with ResourcePlugin#getWorkSpace() method. Click to enlarge
You'll get a New Project with the right click in eclipse.

You can get the project information using this code.

IWorkspace workspace = ResourcesPlugin.getWorkspace();
IWorkspaceRoot root = workspace.getRoot();
// Get all projects in the workspace
IProject[] projects = root.getProjects();

When you know the name of the project, you can find it.

IProject project = root.getProject("Hello");

Out of many project, you need only Java project.

IJavaProject javaProject = JavaCore.create(project);

package fragments, compilation unit

Remember the package explorer in eclipse, you also have the project explorer. Inside a Java project, you'll find a lot of elements, which are called package fragments. From the package fragments, you normally want to use source code. getKind() method returns the property of the package fragment.

IPackageFragment[] packages = javaProject.getPackageFragments();
for (IPackageFragment mypackage : packages) {
    if (mypackage.getKind() == IPackageFragmentRoot.K_SOURCE) {

You can get the ICompilationUnit from package element.

IPackageFragment[] packages = JavaCore.create(project).getPackageFragments();
for (IPackageFragment mypackage : packages) {
	if (mypackage.getKind() == IPackageFragmentRoot.K_SOURCE) {
		for (ICompilationUnit unit : mypackage.getCompilationUnits()) {
			...
		}
	}
}

When you know the name of the type, you can get ICompilationUnit from it.

IType iType = javaProject.findType("PACKAGE_NAME.CLASS_NAME");
org.eclipse.jdt.core.ICompilationUnit iCompilationUnit = iType.getCompilationUnit();

parser and CompilationUnit

CompilationUnit is ASTNode that has the tree inside.

final ASTParser parser = ASTParser.newParser(AST.JLS3); 
parser.setKind(ASTParser.K_COMPILATION_UNIT);
parser.setSource(iCompilationUnit);
parser.setResolveBindings(true); // we need bindings later on
CompilationUnit unit = (CompilationUnit) parser.createAST(null);

Think

• As you instantiate a specific object (JavaProject for example) from other object(Project for example), you can access the elements in the specific object.

References

• Eclipse create CompilationUnit from .java file
• Use ASTParser to Parse a Java Project
• Eclipse JDT - Abstract Syntax Tree (AST) and the Java Model - Tutorial

Eclipse ICompilationUnit

Compared to concrete class CompilationUnit, ICompilation is an interface as the "I" prepended.
It's for Type representation where as CompilationUnit is for AST representation, and parser object links between the two using Parser#setSource(ICompilationUnit); and parser.createAST(null).

In order to get the ICompilationUnit from java source code, you need to start from Workspace, IProject, IJavaProject and then find IType(The by using findType(TYPE_NAME).

References

• How you can get CompilationUnit (AST) from Workspace in eclipse?

Eclipse CompilationUnit

Eclipse uses compilation unit to represent a class. It's reasonable considering one java source generates one class file with the same name (if we forget about the inner class).

One can think of compilation unit in eclipse as a ASTNode for java code as it subclassing ASTNode.

Getting Compilation is a little bit complicated.

• One needs to create a parser as parser has a reference to it. Call parser.createAST() to get CompilationUnit. Don't forget to down casting it to CompilationUnit.
• One needs to setup a parser with the source of ICompilationUnit

And this is the code.

// … lwType is IType object
org.eclipse.jdt.core.ICompilationUnit lwCompilationUnit = lwType.getCompilationUnit();
// create parser and set it up
final ASTParser parser = ASTParser.newParser(AST.JLS3); 
parser.setKind(ASTParser.K_COMPILATION_UNIT);
parser.setSource(lwCompilationUnit);
parser.setResolveBindings(true); // we need bindings later on
// can get CompilationUnit from parser
CompilationUnit unit = (CompilationUnit) parser.createAST(null /* IProgressMonitor */);

References

• Class CompilationUnit
• Eclipse create CompilationUnit from .java file
• How you can get CompilationUnit (AST) from Workspace in eclipse?

Duck Typing

Duck Typing enables Polymorphism without Inheritance.

• http://stackoverflow.com/a/9901670/260127
• http://en.wikipedia.org/wiki/Duck_typing

Polymorphism

In construction …

Inheritance

In construction …