package org.checkerframework.dataflow.cfg.block;

import java.util.List;
import java.util.Set;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.cfg.node.Node;
import org.checkerframework.dataflow.qual.Pure;
import org.plumelib.util.UniqueId;

/** Represents a basic block in a control flow graph. */
public interface Block extends UniqueId {

  /** The types of basic blocks. */
  public static enum BlockType {

    /** A regular basic block. */
    REGULAR_BLOCK,

    /** A conditional basic block. */
    CONDITIONAL_BLOCK,

    /** A special basic block. */
    SPECIAL_BLOCK,

    /** A basic block that can throw an exception. */
    EXCEPTION_BLOCK,
  }

  /**
   * Returns the type of this basic block.
   *
   * @return the type of this basic block
   */
  BlockType getType();

  /**
   * Returns the predecessors of this basic block.
   *
   * @return the predecessors of this basic block
   */
  Set<Block> getPredecessors();

  /**
   * Returns the successors of this basic block.
   *
   * @return the successors of this basic block
   */
  Set<Block> getSuccessors();

  /**
   * Returns the nodes contained within this basic block. The list may be empty.
   *
   * <p>The following invariant holds.
   *
   * <pre>
   * forall n in getNodes() :: n.getBlock() == this
   * </pre>
   *
   * @return the nodes contained within this basic block
   */
  @Pure
  List<Node> getNodes();

  /**
   * Returns the last node of this block, or null if none.
   *
   * @return the last node of this block or {@code null}
   */
  @Nullable Node getLastNode();
}