de.unisaarland.cs.st.jerify.verifier.alias
Class ClassCFGAliasAnalysis

java.lang.Object
  extended by de.unisaarland.cs.st.jerify.verifier.alias.ClassCFGAliasAnalysis

public class ClassCFGAliasAnalysis
extends java.lang.Object

Manages the creation process of AliasAnalysisVarHandle and alias FlowNodes.

Author:
Daniel Wand (typestate@ewand.de)

Constructor Summary
ClassCFGAliasAnalysis()
           
ClassCFGAliasAnalysis(ClassCFGAliasAnalysis copyFrom)
           
 
Method Summary
 TSFlowNode assignment(AliasAnalysisVarHandle handle, com.sun.source.tree.ExpressionTree initTree, MethodCFGWorkData tsinfo)
          //TODO improve Returns a flow node that assigns the init tree value to the variable in handle
 TSFlowNode assignment(com.sun.source.tree.AssignmentTree assignmentTree, MethodCFGWorkData tsinfo)
          Analyse a variable assignment.
 ClassCFGAliasAnalysis copy()
          Creates a deep Copy.
 Pair<TSAliasAnalysisAssignmentFlowNode,AliasAnalysisVarHandle> expression(com.sun.source.tree.ExpressionTree exprTree, MethodCFGWorkData tsinfo)
          Create a new variable handle which is initialized with the result of the analysis of the expression.
 void field(com.sun.source.tree.AssignmentTree assignTree)
          Analyse and add a field.
 void field(javax.lang.model.element.Name name)
           
 void field(com.sun.source.tree.VariableTree varTree)
          Analyse and add a field.
 Pair<TSAliasAnalysisAssignmentFlowNode,java.lang.Integer> foreachVar(com.sun.source.tree.VariableTree varTree)
          Add a for each variable (for var : ... ) to the alias information.
 AliasAnalysisVarHandle getHandle(javax.lang.model.element.Name varName)
          Return the handle for the passed Name.
 AliasAnalysisVarHandle getHandle(java.lang.String varName)
          Return the handle for the passed Name.
 com.sun.source.tree.VariableTree getTree(javax.lang.model.element.Name varName)
          Return the handle for the passed Name.
 com.sun.source.tree.VariableTree getTree(java.lang.String varName)
          Return the handle for the passed Name.
 boolean isField(javax.lang.model.element.Name name)
           
 TSAliasAnalysisAssignmentFlowNode newVar(com.sun.source.tree.VariableTree varTree, MethodCFGWorkData tsinfo)
          Analyse a variable declaration, add the variable to the alias information.
 Pair<TSAliasAnalysisAssignmentFlowNode,AliasAnalysisVarHandle> parameter(com.sun.source.tree.VariableTree varTree)
          Add a parameter to the alias information.
 Pair<TSAliasAnalysisAssignmentFlowNode,AliasAnalysisVarHandle> parameter(com.sun.source.tree.VariableTree varTree, AliasAnalysisVarHandle aliasedTo)
          Add a parameter to the alias information.
 java.util.Set<java.lang.String> without(ClassCFGAliasAnalysis other)
          Returns all names (of variables) that are contained in this AliasAnalysis but not in the passed one and all names that are contained in both but with different AliasVarHandles (which mean that they represent different variables).
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

ClassCFGAliasAnalysis

public ClassCFGAliasAnalysis()

ClassCFGAliasAnalysis

public ClassCFGAliasAnalysis(ClassCFGAliasAnalysis copyFrom)
Method Detail

field

public void field(com.sun.source.tree.VariableTree varTree)
Analyse and add a field.

Parameters:
varTree - the field to analyse.

isField

public boolean isField(javax.lang.model.element.Name name)

field

public void field(com.sun.source.tree.AssignmentTree assignTree)
Analyse and add a field.

Parameters:
varTree - the field to analyse.

field

public void field(javax.lang.model.element.Name name)

foreachVar

public Pair<TSAliasAnalysisAssignmentFlowNode,java.lang.Integer> foreachVar(com.sun.source.tree.VariableTree varTree)
Add a for each variable (for var : ... ) to the alias information.

Parameters:
varTree - the VariableTree that is representing the variable
Returns:
An FlowNode which must be included in the CFG

parameter

public Pair<TSAliasAnalysisAssignmentFlowNode,AliasAnalysisVarHandle> parameter(com.sun.source.tree.VariableTree varTree)
Add a parameter to the alias information. It is assumed that the parameter are pairwise not aliased. And that they do represent an object.

Parameters:
varTree - the VariableTree that is representing the parameter
Returns:
An FlowNode which must be included in the CFG

parameter

public Pair<TSAliasAnalysisAssignmentFlowNode,AliasAnalysisVarHandle> parameter(com.sun.source.tree.VariableTree varTree,
                                                                                AliasAnalysisVarHandle aliasedTo)
Add a parameter to the alias information. It is assumed that the parameter are pairwise not aliased. And that they do represent an object.

Parameters:
varTree - the VariableTree that is representing the parameter
aliasedTo - the variable handle that initializes this parameter
Returns:
An FlowNode which must be included in the CFG

newVar

public TSAliasAnalysisAssignmentFlowNode newVar(com.sun.source.tree.VariableTree varTree,
                                                MethodCFGWorkData tsinfo)
Analyse a variable declaration, add the variable to the alias information. If the variable is initialized an FlowNode for the CFG is returned. If it is not initialized, the variable is not aliased and therefore no FlowNode is needed.

Parameters:
varTree - The variable declaration to be analysed.
Returns:
A FlowNode that represent the initialization of the variable, if one exists.

assignment

public TSFlowNode assignment(com.sun.source.tree.AssignmentTree assignmentTree,
                             MethodCFGWorkData tsinfo)
Analyse a variable assignment. This analyses the assignment, to determine the Sources of aliasing. It then creates a FlowNode that will update the correct handle.

Parameters:
assignmentTree - The assignment to analyse.
Returns:
The FlowNode that must be included in the CFG to update the alias information, accourding to this assingment. Or null if analysis failed.

assignment

public TSFlowNode assignment(AliasAnalysisVarHandle handle,
                             com.sun.source.tree.ExpressionTree initTree,
                             MethodCFGWorkData tsinfo)
//TODO improve Returns a flow node that assigns the init tree value to the variable in handle

Parameters:
handle -
initTree -
Returns:

expression

public Pair<TSAliasAnalysisAssignmentFlowNode,AliasAnalysisVarHandle> expression(com.sun.source.tree.ExpressionTree exprTree,
                                                                                 MethodCFGWorkData tsinfo)
Create a new variable handle which is initialized with the result of the analysis of the expression. It will be initialized by an also create FlowNode.

Parameters:
exprTree - The expression to analyse.
Returns:
An variable handle and a FlowNode which takes care of initializing that handle.

getHandle

public AliasAnalysisVarHandle getHandle(javax.lang.model.element.Name varName)
Return the handle for the passed Name. The Name must be of a variable or parameter added with the corresponding methods.

Parameters:
varName - the Name of the handle
Returns:
the varialbe handle for that name, if one exists.

getHandle

public AliasAnalysisVarHandle getHandle(java.lang.String varName)
Return the handle for the passed Name. The Name must be of a variable or parameter added with the corresponding methods.

Parameters:
varName - the Name of the handle
Returns:
the varialbe handle for that name, if one exists.

getTree

public com.sun.source.tree.VariableTree getTree(javax.lang.model.element.Name varName)
Return the handle for the passed Name. The Name must be of a variable or parameter added with the corresponding methods.

Parameters:
varName - the Name of the handle
Returns:
the varialbe handle for that name, if one exists.

getTree

public com.sun.source.tree.VariableTree getTree(java.lang.String varName)
Return the handle for the passed Name. The Name must be of a variable or parameter added with the corresponding methods.

Parameters:
varName - the Name of the handle
Returns:
the varialbe handle for that name, if one exists.

copy

public ClassCFGAliasAnalysis copy()
Creates a deep Copy. Each (java language) block should get its own copy of the CFGAliasAnalysis.


without

public java.util.Set<java.lang.String> without(ClassCFGAliasAnalysis other)
Returns all names (of variables) that are contained in this AliasAnalysis but not in the passed one and all names that are contained in both but with different AliasVarHandles (which mean that they represent different variables).

Parameters:
other - The analysis to compare with
Returns:
The names in this but not in the passed AliasAnalysis