org.checkerframework.dataflow.cfg

Class CFGBuilder

java.lang.Object

org.checkerframework.dataflow.cfg.CFGBuilder

Direct Known Subclasses:

CFCFGBuilder

public class CFGBuilder
extends java.lang.Object

Builds the control flow graph of some Java code (either a method, or an arbitrary statement).

The translation of the AST to the CFG is split into three phases:

1. Phase one. In the first phase, the AST is translated into a sequence of CFGBuilder.ExtendedNodes. An extended node can either be a Node, or one of several meta elements such as a conditional or unconditional jump or a node with additional information about exceptions. Some of the extended nodes contain labels (e.g., for the jump target), and phase one additionally creates a mapping from labels to extended nodes. Finally, the list of leaders is computed: A leader is an extended node which will give rise to a basic block in phase two.
2. Phase two. In this phase, the sequence of extended nodes is translated to a graph of control flow blocks that contain nodes. The meta elements from phase one are translated into the correct edges.
3. Phase three. The control flow graph generated in phase two can contain degenerate basic blocks such as empty regular basic blocks or conditional basic blocks that have the same block as both 'then' and 'else' successor. This phase removes these cases while preserving the control flow structure.

Author:

Stefan Heule

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
class	CFGBuilder.CFGTranslationPhaseOne Class that performs phase one of the translation process.
static class	CFGBuilder.CFGTranslationPhaseThree Class that performs phase three of the translation process.
class	CFGBuilder.CFGTranslationPhaseTwo Class that performs phase two of the translation process.
protected static class	CFGBuilder.ConditionalJump An extended node of type CFGBuilder.ExtendedNode.ExtendedNodeType.CONDITIONAL_JUMP.
protected static class	CFGBuilder.ExtendedNode An extended node can be one of several things (depending on its type): NODE.
protected static class	CFGBuilder.Label A label is used to refer to other extended nodes using a mapping from labels to extended nodes.
protected static class	CFGBuilder.NodeHolder An extended node of type NODE.
protected static class	CFGBuilder.NodeWithExceptionsHolder An extended node of type EXCEPTION_NODE.
protected static class	CFGBuilder.PhaseOneResult A wrapper object to pass around the result of phase one.
protected static class	CFGBuilder.TryCatchFrame A TryCatchFrame contains an ordered list of catch labels that apply to exceptions with specific types.
protected static class	CFGBuilder.TryFinallyFrame A TryFinallyFrame applies to exceptions of any type
protected static interface	CFGBuilder.TryFrame A TryFrame takes a thrown exception type and maps it to a set of possible control-flow successors.
protected static class	CFGBuilder.TryStack An exception stack represents the set of all try-catch blocks in effect at a given point in a program.
protected static class	CFGBuilder.Tuple<A,B,C> Tuple class with up to three members.
protected static class	CFGBuilder.UnconditionalJump An extended node of type CFGBuilder.ExtendedNode.ExtendedNodeType.UNCONDITIONAL_JUMP.

Field Summary

Fields

Modifier and Type	Field and Description
protected boolean	assumeAssertionsDisabled Can assertions be assumed to be disabled?
protected boolean	assumeAssertionsEnabled Can assertions be assumed to be enabled?
protected java.util.List<com.sun.source.tree.ClassTree>	declaredClasses Class declarations that have been encountered when building the control-flow graph for a method.
protected java.util.List<com.sun.source.tree.LambdaExpressionTree>	declaredLambdas Lambdas encountered when building the control-flow graph for a method, variable initializer, or initializer.
protected CFGBuilder.Label	exceptionalExitLabel Special label to identify the exceptional exit.
protected CFGBuilder.Label	regularExitLabel Special label to identify the regular exit.

Constructor Summary

Constructors

Constructor and Description
CFGBuilder(boolean assumeAssertionsEnabled, boolean assumeAssertionsDisabled)

Method Summary

Modifier and Type	Method and Description
static ControlFlowGraph	build(com.sun.source.tree.CompilationUnitTree root, javax.annotation.processing.ProcessingEnvironment env, com.sun.source.tree.MethodTree tree, com.sun.source.tree.ClassTree classTree) Build the control flow graph of a method.
static ControlFlowGraph	build(com.sun.source.tree.CompilationUnitTree root, javax.annotation.processing.ProcessingEnvironment env, com.sun.source.tree.MethodTree tree, com.sun.source.tree.ClassTree classTree, boolean assumeAssertionsEnabled, boolean assumeAssertionsDisabled) Build the control flow graph of a method.
static ControlFlowGraph	build(com.sun.source.tree.CompilationUnitTree root, javax.annotation.processing.ProcessingEnvironment env, UnderlyingAST underlyingAST) Build the control flow graph of some code.
static ControlFlowGraph	build(com.sun.source.tree.CompilationUnitTree root, javax.annotation.processing.ProcessingEnvironment env, UnderlyingAST underlyingAST, boolean assumeAssertionsEnabled, boolean assumeAssertionsDisabled) Build the control flow graph of some code.
static ControlFlowGraph	build(com.sun.source.util.TreePath bodyPath, javax.annotation.processing.ProcessingEnvironment env, UnderlyingAST underlyingAST, boolean assumeAssertionsEnabled, boolean assumeAssertionsDisabled) Build the control flow graph of some code (method, initializer block, ...).
java.util.List<com.sun.source.tree.ClassTree>	getDeclaredClasses()
java.util.List<com.sun.source.tree.LambdaExpressionTree>	getDeclaredLambdas()
protected static void	printBlocks(java.util.Set<Block> blocks) Print a set of Blocks and the edges between them.
ControlFlowGraph	run(com.sun.source.tree.CompilationUnitTree root, javax.annotation.processing.ProcessingEnvironment env, com.sun.source.tree.MethodTree tree, com.sun.source.tree.ClassTree classTree) Build the control flow graph of a method.
ControlFlowGraph	run(com.sun.source.tree.CompilationUnitTree root, javax.annotation.processing.ProcessingEnvironment env, UnderlyingAST underlyingAST) Build the control flow graph of some code.
ControlFlowGraph	run(com.sun.source.util.TreePath bodyPath, javax.annotation.processing.ProcessingEnvironment env, UnderlyingAST underlyingAST) Build the control flow graph of some code (method, initializer block, ...).

Methods inherited from class java.lang.Object

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

Field Detail

assumeAssertionsDisabled

protected final boolean assumeAssertionsDisabled

Can assertions be assumed to be disabled?

assumeAssertionsEnabled

protected final boolean assumeAssertionsEnabled

Can assertions be assumed to be enabled?

declaredClasses

protected final java.util.List<com.sun.source.tree.ClassTree> declaredClasses

Class declarations that have been encountered when building the control-flow graph for a method.

declaredLambdas

protected final java.util.List<com.sun.source.tree.LambdaExpressionTree> declaredLambdas

Lambdas encountered when building the control-flow graph for a method, variable initializer, or initializer.

exceptionalExitLabel

protected final CFGBuilder.Label exceptionalExitLabel

Special label to identify the exceptional exit.

regularExitLabel

protected final CFGBuilder.Label regularExitLabel

Special label to identify the regular exit.

Constructor Detail

CFGBuilder

public CFGBuilder(boolean assumeAssertionsEnabled,
                  boolean assumeAssertionsDisabled)

Method Detail

getDeclaredClasses

public java.util.List<com.sun.source.tree.ClassTree> getDeclaredClasses()

getDeclaredLambdas

public java.util.List<com.sun.source.tree.LambdaExpressionTree> getDeclaredLambdas()

build

public static ControlFlowGraph build(com.sun.source.tree.CompilationUnitTree root,
                                     javax.annotation.processing.ProcessingEnvironment env,
                                     UnderlyingAST underlyingAST,
                                     boolean assumeAssertionsEnabled,
                                     boolean assumeAssertionsDisabled)

Build the control flow graph of some code.

build

public static ControlFlowGraph build(com.sun.source.util.TreePath bodyPath,
                                     javax.annotation.processing.ProcessingEnvironment env,
                                     UnderlyingAST underlyingAST,
                                     boolean assumeAssertionsEnabled,
                                     boolean assumeAssertionsDisabled)

Build the control flow graph of some code (method, initializer block, ...). bodyPath is the TreePath to the body of that code.

build

public static ControlFlowGraph build(com.sun.source.tree.CompilationUnitTree root,
                                     javax.annotation.processing.ProcessingEnvironment env,
                                     com.sun.source.tree.MethodTree tree,
                                     com.sun.source.tree.ClassTree classTree,
                                     boolean assumeAssertionsEnabled,
                                     boolean assumeAssertionsDisabled)

Build the control flow graph of a method.

build

public static ControlFlowGraph build(com.sun.source.tree.CompilationUnitTree root,
                                     javax.annotation.processing.ProcessingEnvironment env,
                                     UnderlyingAST underlyingAST)

Build the control flow graph of some code.

build

public static ControlFlowGraph build(com.sun.source.tree.CompilationUnitTree root,
                                     javax.annotation.processing.ProcessingEnvironment env,
                                     com.sun.source.tree.MethodTree tree,
                                     com.sun.source.tree.ClassTree classTree)

Build the control flow graph of a method.

run

public ControlFlowGraph run(com.sun.source.tree.CompilationUnitTree root,
                            javax.annotation.processing.ProcessingEnvironment env,
                            UnderlyingAST underlyingAST)

Build the control flow graph of some code.

run

public ControlFlowGraph run(com.sun.source.util.TreePath bodyPath,
                            javax.annotation.processing.ProcessingEnvironment env,
                            UnderlyingAST underlyingAST)

Build the control flow graph of some code (method, initializer block, ...). bodyPath is the TreePath to the body of that code.

run

public ControlFlowGraph run(com.sun.source.tree.CompilationUnitTree root,
                            javax.annotation.processing.ProcessingEnvironment env,
                            com.sun.source.tree.MethodTree tree,
                            com.sun.source.tree.ClassTree classTree)

Build the control flow graph of a method.

printBlocks

protected static void printBlocks(java.util.Set<Block> blocks)

Print a set of Blocks and the edges between them. This is useful for examining the results of phase two.