Class CFGTranslationPhaseThree

java.lang.Object
org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseThree

public class CFGTranslationPhaseThree extends 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.
  • Constructor Details

    • CFGTranslationPhaseThree

      public CFGTranslationPhaseThree()
  • Method Details

    • 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, Set<RegularBlockImpl> emptyBlocks, Set<CFGTranslationPhaseThree.PredecessorHolder> predecessors)
      Compute the set of empty regular basic blocks emptyBlocks, 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)
      emptyBlocks - 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
      Returns:
      the single successor of the set of the empty basic blocks
    • computeNeighborhoodOfEmptyBlockBackwards

      protected static void computeNeighborhoodOfEmptyBlockBackwards(RegularBlockImpl start, Set<RegularBlockImpl> emptyBlocks, Set<CFGTranslationPhaseThree.PredecessorHolder> predecessors)
      Compute the set of empty regular basic blocks emptyBlocks, 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)
      emptyBlocks - 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 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).
      Parameters:
      pred - a block whose successor should be set
      cur - the previous successor of pred
      Returns:
      a predecessor holder to set the successor of pred
    • singleSuccessorHolder

      protected static CFGTranslationPhaseThree.PredecessorHolder singleSuccessorHolder(SingleSuccessorBlockImpl s, BlockImpl old)
      Returns a CFGTranslationPhaseThree.PredecessorHolder that sets the successor of a single successor block s.
      Returns:
      a CFGTranslationPhaseThree.PredecessorHolder that sets the successor of a single successor block s