The typestate checking tool checks protocols that each object of a class has to obey. The tool can check protocols that can be expressed as automatons. To provide the tool with the protocol it has to check, methods can be annotated with three java annotations.

The checker itself uses different phases to analyse a program.
(1) Creating a Control Flow Graph of the method that is analysed
(2) Analaysing the method using that Graph.

Overview

To analyse a program the checker analyses each class and within each class each method separately.
For each compilation unit root the checker runs a visitor (CompilationUnitCFG) that visits each class in that compilation unit. The CompilationUnit Visitor then creates a visitor that visit each class separately. This visitor (ClassCFG) creates a control flow graph data structure for each method that contains all typestate and local aliasing tracking. This graph is then used to analyse the method. The graph nodes have distinct functionality the and propagate the analysis data through the graph until a fixpoint is reached, this fixpoint is the desired analysis.

Java Constructs

For each java language construct certain nodes and connection between those nodes are inserted.

For example a method will have two nodes and the control flow graph that follows from its block:

                -> [method begin node] -> [methd block cfg] -> [method end node]

As we only analyse methods, the method begin node will always be the first node in the graph, likewise the method end node that last node. To start an analysis we can pass an empty anlysis data to the method begin node, which will propagte it to its successor, its successors to their succesors ...

Other java constructs:
The if construct will have a condition and then branch into two different control flow graphs for the true and
false branch and then merge those together:

                     ↑-------> [true branch cfg ] ----↓
                -> [cond]                          [merge] ->
                     ↓-------> [false branch cfg] ----↑
        

The [cond] node will generate copies of the analysis it receives and will pass each branch its own analysis, the branches then pass their analysis on to the [merge] node. The [merge] then will pass it to the statement that follows the if.

For the other java language constructs see the ClassCFG class and the visit* methods.

Now we are not only interested in the shape of the java code, but also on its aliasing and typestate behavior.

Aliasing

To track the local alias flow, we try to track the potential flow of objects. So each variable is tracked, and for each assignment the appropriate changes to the alias information is made.
This is done by simply integrating alias nodes at the points of assignment into the control flow graph. see ClassCFG visitVariable/Assignment and TSAliasAnalysisAssignmentFlowNode.

E.g.
Assignment:
 var a= b; will be encoded as an TSAliasAnalysisAssignmentFlowNode in the graph, so when the analysis is propagatet it will look up the currently "known" abstract objects of by and assign them also to a.

Typestate

The typestate of an object is changed only if a method is invocated on it. So each method invocation is translated into a node that will find out the alias objects assigned to the reciever, and a node that will change the typestate of those objects. See ClassCFG visitMethodInvocation for details.

The Control Flow Graph Nodes are in the flownodes package (and subpackages 1 2). For the Typestate flownodes TSStateChangingFlowNode contains the factory method to create the FlowNodes that actually influcence the typestate. Also normal usage will call TSFlowNode factory methods (for state changing FlowNodes it forwards those calls to TSStateChaningFlowNode).

The Graph is constructed by the ClassCFG which is in the typestate package. In that package are also all datastructures that are used to create the CFG. (But not the
CFG datastructures themself). The datastructure that is propagated thrugh the graph is the MethodTypestateAnalysis class.

 There are several JUnit tests that tests most of the checkers functionallity. The field tests are expected to fail (as it is not implemented yet).