org.checkerframework.dataflow.cfg

Class CFGBuilder.CFGTranslationPhaseThree

java.lang.Object

org.checkerframework.dataflow.cfg.CFGBuilder.CFGTranslationPhaseThree

Enclosing class:

CFGBuilder

public static class CFGBuilder.CFGTranslationPhaseThree
extends java.lang.Object

Class that performs phase three of the translation process. In particular, the following degenerate cases of basic blocks are removed:

1. Empty regular basic blocks: These blocks will be removed and their predecessors linked directly to the successor.
2. Conditional basic blocks that have the same basic block as the 'then' and 'else' successor: The conditional basic block will be removed in this case.
3. Two consecutive, non-empty, regular basic blocks where the second block has exactly one predecessor (namely the other of the two blocks): In this case, the two blocks are merged.
4. Some basic blocks might not be reachable from the entryBlock. These basic blocks are removed, and the list of predecessors (in the doubly-linked structure of basic blocks) are adapted correctly.

Eliminating the second type of degenerate cases might introduce cases of the third problem. These are also removed.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static interface	CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder A simple wrapper object that holds a basic block and allows to set one of its successors.

Constructor Summary

Constructors

Constructor and Description
CFGTranslationPhaseThree()

Method Summary

Modifier and Type	Method and Description
protected static BlockImpl	computeNeighborhoodOfEmptyBlock(RegularBlockImpl start, java.util.Set<RegularBlockImpl> empty, java.util.Set<CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder> predecessors) Compute the set of empty regular basic blocks empty, starting at start and going both forward and backwards.
protected static void	computeNeighborhoodOfEmptyBlockBackwards(RegularBlockImpl start, java.util.Set<RegularBlockImpl> empty, java.util.Set<CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder> predecessors) Compute the set of empty regular basic blocks empty, starting at start and looking only backwards in the control flow graph.
protected static CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder	getPredecessorHolder(BlockImpl pred, BlockImpl cur) Return a predecessor holder that can be used to set the successor of pred in the place where previously the edge pointed to cur.
static ControlFlowGraph	process(ControlFlowGraph cfg) Perform phase three on the control flow graph cfg.
protected static CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder	singleSuccessorHolder(SingleSuccessorBlockImpl s, BlockImpl old)

Methods inherited from class java.lang.Object

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

Constructor Detail

CFGTranslationPhaseThree

public CFGTranslationPhaseThree()

Method Detail

process

public static ControlFlowGraph process(ControlFlowGraph cfg)

Perform phase three on the control flow graph cfg.

Parameters:

cfg - the control flow graph. Ownership is transfered to this method and the caller is not allowed to read or modify cfg after the call to process any more.

Returns:

the resulting control flow graph

computeNeighborhoodOfEmptyBlock

protected static BlockImpl computeNeighborhoodOfEmptyBlock(RegularBlockImpl start,
                                                           java.util.Set<RegularBlockImpl> empty,
                                                           java.util.Set<CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder> predecessors)

Compute the set of empty regular basic blocks empty, starting at start and going both forward and backwards. Furthermore, compute the predecessors of these empty blocks (predecessors ), and their single successor (return value).

Parameters:

start - the starting point of the search (an empty, regular basic block)

empty - an empty set to be filled by this method with all empty basic blocks found (including start).

predecessors - an empty set to be filled by this method with all predecessors

Returns:

the single successor of the set of the empty basic blocks

computeNeighborhoodOfEmptyBlockBackwards

protected static void computeNeighborhoodOfEmptyBlockBackwards(RegularBlockImpl start,
                                                               java.util.Set<RegularBlockImpl> empty,
                                                               java.util.Set<CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder> predecessors)

Compute the set of empty regular basic blocks empty, starting at start and looking only backwards in the control flow graph. Furthermore, compute the predecessors of these empty blocks ( predecessors).

Parameters:

start - the starting point of the search (an empty, regular basic block)

empty - a set to be filled by this method with all empty basic blocks found (including start).

predecessors - a set to be filled by this method with all predecessors

getPredecessorHolder

protected static CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder getPredecessorHolder(BlockImpl pred,
                                                                                            BlockImpl cur)

Return a predecessor holder that can be used to set the successor of pred in the place where previously the edge pointed to cur. Additionally, the predecessor holder also takes care of unlinking (i.e., removing the pred from cur's predecessors).

singleSuccessorHolder

protected static CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder singleSuccessorHolder(SingleSuccessorBlockImpl s,
                                                                                             BlockImpl old)

Returns:

a CFGBuilder.CFGTranslationPhaseThree.PredecessorHolder that sets the successor of a single successor block s.