de.unisaarland.cs.st.jerify.verifier.typestate
Class ClassCFG

java.lang.Object
  com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>
      de.unisaarland.cs.st.jerify.verifier.typestate.ClassCFG

All Implemented Interfaces:

com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

public class ClassCFG
extends com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

Creates the typestate check data structure ClassCFGData for a class and its subclasses, it does so by creating a control flow graph data structure for each method MethodCFGData. The flow data structure consists of FlowNodes, which replicate the flow structure of the underlying Java code and incorporate alias and typestate tracking. It is created while running the Visitor on the ClassTree representing the class. visitClass and scanMethod create the corresponding ClassCFGData respectively MethodCFGData, all other visit* methods create and link the FlowNodes. The information created while visiting is stored in the TSInfos MethodCFGWorkData data structure, this is only the work data for constructing the ClassCFGData/MethodCFGData.

Author:

Daniel Wand (typestate@ewand.de)

Constructor Summary

ClassCFG(java.lang.String qualifiedPackageName, checkers.types.AnnotatedTypeFactory factory)
Create a TSMapping which typestate-checks the CompilationUnitTree.

Method Summary

MethodCFGData	scanMethod(com.sun.source.tree.MethodTree tree, MethodCFGWorkData tsinfo) For each method, create the flow data structure relations TSFlowNode and return it in the MethodCFGData.
ClassCFGData	visitAnnotation(com.sun.source.tree.AnnotationTree arg0, MethodCFGWorkData arg1) Skip analysis of annotations, so we do not have to case about @annotaion( is="bla") assignments in visitAssingment
ClassCFGData	visitAssignment(com.sun.source.tree.AssignmentTree tree, MethodCFGWorkData tsinfo) Visit assignments and create FlowNodes that update alias information accordingly
ClassCFGData	visitBlock(com.sun.source.tree.BlockTree tree, MethodCFGWorkData tsinfo) Create a new work-data aliasAnalysis for each block, so the variables that with scope of a block will be removed after each block
ClassCFGData	visitBreak(com.sun.source.tree.BreakTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow changes caused by break
ClassCFGData	visitClass(com.sun.source.tree.ClassTree node, MethodCFGWorkData tsinfo) Create the ClassCFGData from the node that is passed.
ClassCFGData	visitConditionalExpression(com.sun.source.tree.ConditionalExpressionTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow implications for the analysis caused by conditional expressions
ClassCFGData	visitContinue(com.sun.source.tree.ContinueTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow changes caused by continue
ClassCFGData	visitDoWhileLoop(com.sun.source.tree.DoWhileLoopTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow changes caused by a do-while loop
ClassCFGData	visitEnhancedForLoop(com.sun.source.tree.EnhancedForLoopTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow changes caused by a enhanced for loop Actually currently the checker needs a @SetState annotation on the loop variable, the rational being that one can more easily annotate the loop variable but may have a hard time annotating the iterator.
ClassCFGData	visitForLoop(com.sun.source.tree.ForLoopTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow changes caused by a for loop
ClassCFGData	visitIf(com.sun.source.tree.IfTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow implications for the analysis caused by if statements
ClassCFGData	visitLabeledStatement(com.sun.source.tree.LabeledStatementTree tree, MethodCFGWorkData tsinfo) Analyse the body of the the label statement with the knowledge about that label.
ClassCFGData	visitMethodInvocation(com.sun.source.tree.MethodInvocationTree tree, MethodCFGWorkData tsinfo) Analyse method invocations and create FlowNodes that track typestate changes.
ClassCFGData	visitNewClass(com.sun.source.tree.NewClassTree node, MethodCFGWorkData tsinfo)
ClassCFGData	visitReturn(com.sun.source.tree.ReturnTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow implications for the analysis caused by return statements
ClassCFGData	visitSwitch(com.sun.source.tree.SwitchTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow implications for the analysis caused by switch statements
ClassCFGData	visitThrow(com.sun.source.tree.ThrowTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow implications for the analysis caused by throw statements
ClassCFGData	visitTry(com.sun.source.tree.TryTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow implications for the analysis caused by try-catch-finally statements
ClassCFGData	visitVariable(com.sun.source.tree.VariableTree tree, MethodCFGWorkData tsinfo) Parse variable / fields and create alias information / flownodes accordingly
ClassCFGData	visitWhileLoop(com.sun.source.tree.WhileLoopTree tree, MethodCFGWorkData tsinfo) Create FlowNodes that handle the control flow changes caused by a while loop

Methods inherited from class com.sun.source.util.TreeScanner

reduce, scan, scan, visitAnnotatedType, visitArrayAccess, visitArrayType, visitAssert, visitBinary, visitCase, visitCatch, visitCompilationUnit, visitCompoundAssignment, visitEmptyStatement, visitErroneous, visitExpressionStatement, visitIdentifier, visitImport, visitInstanceOf, visitLiteral, visitMemberSelect, visitMethod, visitModifiers, visitNewArray, visitOther, visitParameterizedType, visitParenthesized, visitPrimitiveType, visitSynchronized, visitTypeCast, visitTypeParameter, visitUnary, visitWildcard

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ClassCFG

public ClassCFG(java.lang.String qualifiedPackageName,
                checkers.types.AnnotatedTypeFactory factory)

Create a TSMapping which typestate-checks the CompilationUnitTree.

Parameters:

checker - used to initialize the SourceVisitor (This is the checkers checker so Checker in our case)

factory - The AnnotatedTypeFactory of the checker

root - used to initialize the SourceVisitor (This is the root from which we will descend and create the data structure)

Method Detail

visitClass

public ClassCFGData visitClass(com.sun.source.tree.ClassTree node,
                               MethodCFGWorkData tsinfo)

Create the ClassCFGData from the node that is passed. Is called by the visitor, not directly.

Specified by:

visitClass in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitClass in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

Parameters:

node - the tree repesenting the class.

tsinfo - the data that all the other visit* methods use to create a control flow graph

Returns:

The data structure that includes all CFGs created for this class.

scanMethod

public final MethodCFGData scanMethod(com.sun.source.tree.MethodTree tree,
                                      MethodCFGWorkData tsinfo)

For each method, create the flow data structure relations TSFlowNode and return it in the MethodCFGData.

Parameters:

tree - the method to analyse.

tsinfo - the working data

Returns:

the control flow graph

visitVariable

public ClassCFGData visitVariable(com.sun.source.tree.VariableTree tree,
                                  MethodCFGWorkData tsinfo)

Parse variable / fields and create alias information / flownodes accordingly

Specified by:

visitVariable in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitVariable in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitAnnotation

public ClassCFGData visitAnnotation(com.sun.source.tree.AnnotationTree arg0,
                                    MethodCFGWorkData arg1)

Skip analysis of annotations, so we do not have to case about @annotaion( is="bla") assignments in visitAssingment

Specified by:

visitAnnotation in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitAnnotation in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitAssignment

public ClassCFGData visitAssignment(com.sun.source.tree.AssignmentTree tree,
                                    MethodCFGWorkData tsinfo)

Visit assignments and create FlowNodes that update alias information accordingly

Specified by:

visitAssignment in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitAssignment in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitBlock

public final ClassCFGData visitBlock(com.sun.source.tree.BlockTree tree,
                                     MethodCFGWorkData tsinfo)

Create a new work-data aliasAnalysis for each block, so the variables that with scope of a block will be removed after each block

Specified by:

visitBlock in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitBlock in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitBreak

public final ClassCFGData visitBreak(com.sun.source.tree.BreakTree tree,
                                     MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow changes caused by break

Specified by:

visitBreak in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitBreak in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitConditionalExpression

public final ClassCFGData visitConditionalExpression(com.sun.source.tree.ConditionalExpressionTree tree,
                                                     MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow implications for the analysis caused by conditional expressions

Specified by:

visitConditionalExpression in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitConditionalExpression in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitContinue

public final ClassCFGData visitContinue(com.sun.source.tree.ContinueTree tree,
                                        MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow changes caused by continue

Specified by:

visitContinue in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitContinue in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitDoWhileLoop

public final ClassCFGData visitDoWhileLoop(com.sun.source.tree.DoWhileLoopTree tree,
                                           MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow changes caused by a do-while loop

Specified by:

visitDoWhileLoop in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitDoWhileLoop in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitEnhancedForLoop

public final ClassCFGData visitEnhancedForLoop(com.sun.source.tree.EnhancedForLoopTree tree,
                                               MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow changes caused by a enhanced for loop Actually currently the checker needs a @SetState annotation on the loop variable, the rational being that one can more easily annotate the loop variable but may have a hard time annotating the iterator. This behavior may change if the checker auto-generates annotation and does not require a fully annotated program.

Specified by:

visitEnhancedForLoop in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitEnhancedForLoop in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitForLoop

public final ClassCFGData visitForLoop(com.sun.source.tree.ForLoopTree tree,
                                       MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow changes caused by a for loop

Specified by:

visitForLoop in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitForLoop in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitIf

public final ClassCFGData visitIf(com.sun.source.tree.IfTree tree,
                                  MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow implications for the analysis caused by if statements

Specified by:

visitIf in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitIf in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitLabeledStatement

public final ClassCFGData visitLabeledStatement(com.sun.source.tree.LabeledStatementTree tree,
                                                MethodCFGWorkData tsinfo)

Analyse the body of the the label statement with the knowledge about that label.

Specified by:

visitLabeledStatement in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitLabeledStatement in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitMethodInvocation

public final ClassCFGData visitMethodInvocation(com.sun.source.tree.MethodInvocationTree tree,
                                                MethodCFGWorkData tsinfo)

Analyse method invocations and create FlowNodes that track typestate changes.

Specified by:

visitMethodInvocation in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitMethodInvocation in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitNewClass

public ClassCFGData visitNewClass(com.sun.source.tree.NewClassTree node,
                                  MethodCFGWorkData tsinfo)

Specified by:

visitNewClass in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitNewClass in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitReturn

public final ClassCFGData visitReturn(com.sun.source.tree.ReturnTree tree,
                                      MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow implications for the analysis caused by return statements

Specified by:

visitReturn in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitReturn in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitSwitch

public final ClassCFGData visitSwitch(com.sun.source.tree.SwitchTree tree,
                                      MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow implications for the analysis caused by switch statements

Specified by:

visitSwitch in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitSwitch in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitThrow

public final ClassCFGData visitThrow(com.sun.source.tree.ThrowTree tree,
                                     MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow implications for the analysis caused by throw statements

Specified by:

visitThrow in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitThrow in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitTry

public final ClassCFGData visitTry(com.sun.source.tree.TryTree tree,
                                   MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow implications for the analysis caused by try-catch-finally statements

Specified by:

visitTry in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitTry in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>

visitWhileLoop

public final ClassCFGData visitWhileLoop(com.sun.source.tree.WhileLoopTree tree,
                                         MethodCFGWorkData tsinfo)

Create FlowNodes that handle the control flow changes caused by a while loop

Specified by:

visitWhileLoop in interface com.sun.source.tree.TreeVisitor<ClassCFGData,MethodCFGWorkData>

Overrides:

visitWhileLoop in class com.sun.source.util.TreeScanner<ClassCFGData,MethodCFGWorkData>