Update to version 2.4.0 of Checker Framework dataflow and javacutil

Change-Id: I29e007625d0a25279d8b2967f89b1014b4825bd6

12 files changed, 0 insertions, 500 deletions

diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/Block.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/Block.java
deleted file mode 100644
index 2d58550568..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/Block.java
+++ /dev/null
@@ -1,31 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-/**
- * Represents a basic block in a control flow graph.
- *
- * @author Stefan Heule
- */
-public interface Block {
-
-    /** 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,
-    }
-
-    /** @return the type of this basic block */
-    BlockType getType();
-
-    /** @return the unique identifier of this block */
-    long getId();
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/BlockImpl.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/BlockImpl.java
deleted file mode 100644
index 0421a1e3f5..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/BlockImpl.java
+++ /dev/null
@@ -1,57 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-import java.util.Collections;
-import java.util.HashSet;
-import java.util.Set;
-
-/**
- * Base class of the {@link Block} implementation hierarchy.
- *
- * @author Stefan Heule
- */
-public abstract class BlockImpl implements Block {
-
-    /** A unique ID for this node. */
-    protected long id = BlockImpl.uniqueID();
-
-    /** The last ID that has already been used. */
-    protected static long lastId = 0;
-
-    /** The type of this basic block. */
-    protected BlockType type;
-
-    /** The set of predecessors. */
-    protected Set<BlockImpl> predecessors;
-
-    /** @return a fresh identifier */
-    private static long uniqueID() {
-        return lastId++;
-    }
-
-    public BlockImpl() {
-        predecessors = new HashSet<>();
-    }
-
-    @Override
-    public long getId() {
-        return id;
-    }
-
-    @Override
-    public BlockType getType() {
-        return type;
-    }
-
-    /** @return the list of predecessors of this basic block */
-    public Set<BlockImpl> getPredecessors() {
-        return Collections.unmodifiableSet(predecessors);
-    }
-
-    public void addPredecessor(BlockImpl pred) {
-        predecessors.add(pred);
-    }
-
-    public void removePredecessor(BlockImpl pred) {
-        predecessors.remove(pred);
-    }
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ConditionalBlock.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ConditionalBlock.java
deleted file mode 100644
index dce04abdfe..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ConditionalBlock.java
+++ /dev/null
@@ -1,30 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-import org.checkerframework.dataflow.analysis.Store;
-import org.checkerframework.dataflow.cfg.node.Node;
-
-/**
- * Represents a conditional basic block that contains exactly one boolean {@link Node}.
- *
- * @author Stefan Heule
- */
-public interface ConditionalBlock extends Block {
-
-    /** @return the entry block of the then branch */
-    Block getThenSuccessor();
-
-    /** @return the entry block of the else branch */
-    Block getElseSuccessor();
-
-    /** @return the flow rule for information flowing from this block to its then successor */
-    Store.FlowRule getThenFlowRule();
-
-    /** @return the flow rule for information flowing from this block to its else successor */
-    Store.FlowRule getElseFlowRule();
-
-    /** Set the flow rule for information flowing from this block to its then successor. */
-    void setThenFlowRule(Store.FlowRule rule);
-
-    /** Set the flow rule for information flowing from this block to its else successor. */
-    void setElseFlowRule(Store.FlowRule rule);
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ConditionalBlockImpl.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ConditionalBlockImpl.java
deleted file mode 100644
index bd12522983..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ConditionalBlockImpl.java
+++ /dev/null
@@ -1,81 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-import org.checkerframework.dataflow.analysis.Store;
-
-/**
- * Implementation of a conditional basic block.
- *
- * @author Stefan Heule
- */
-public class ConditionalBlockImpl extends BlockImpl implements ConditionalBlock {
-
-    /** Successor of the then branch. */
-    protected BlockImpl thenSuccessor;
-
-    /** Successor of the else branch. */
-    protected BlockImpl elseSuccessor;
-
-    /**
-     * The rules below say that the THEN store before a conditional block flows to BOTH of the
-     * stores of the then successor, while the ELSE store before a conditional block flows to BOTH
-     * of the stores of the else successor.
-     */
-    protected Store.FlowRule thenFlowRule = Store.FlowRule.THEN_TO_BOTH;
-
-    protected Store.FlowRule elseFlowRule = Store.FlowRule.ELSE_TO_BOTH;
-
-    /**
-     * Initialize an empty conditional basic block to be filled with contents and linked to other
-     * basic blocks later.
-     */
-    public ConditionalBlockImpl() {
-        type = BlockType.CONDITIONAL_BLOCK;
-    }
-
-    /** Set the then branch successor. */
-    public void setThenSuccessor(BlockImpl b) {
-        thenSuccessor = b;
-        b.addPredecessor(this);
-    }
-
-    /** Set the else branch successor. */
-    public void setElseSuccessor(BlockImpl b) {
-        elseSuccessor = b;
-        b.addPredecessor(this);
-    }
-
-    @Override
-    public Block getThenSuccessor() {
-        return thenSuccessor;
-    }
-
-    @Override
-    public Block getElseSuccessor() {
-        return elseSuccessor;
-    }
-
-    @Override
-    public Store.FlowRule getThenFlowRule() {
-        return thenFlowRule;
-    }
-
-    @Override
-    public Store.FlowRule getElseFlowRule() {
-        return elseFlowRule;
-    }
-
-    @Override
-    public void setThenFlowRule(Store.FlowRule rule) {
-        thenFlowRule = rule;
-    }
-
-    @Override
-    public void setElseFlowRule(Store.FlowRule rule) {
-        elseFlowRule = rule;
-    }
-
-    @Override
-    public String toString() {
-        return "ConditionalBlock()";
-    }
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ExceptionBlock.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ExceptionBlock.java
deleted file mode 100644
index a549c5f03f..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ExceptionBlock.java
+++ /dev/null
@@ -1,27 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-import java.util.Map;
-import java.util.Set;
-import javax.lang.model.type.TypeMirror;
-import org.checkerframework.dataflow.cfg.node.Node;
-
-/**
- * Represents a basic block that contains exactly one {@link Node} which can throw an exception.
- * This block has exactly one non-exceptional successor, and one or more exceptional successors.
- *
- * <p>The following invariant holds.
- *
- * <pre>
- * getNode().getBlock() == this
- * </pre>
- *
- * @author Stefan Heule
- */
-public interface ExceptionBlock extends SingleSuccessorBlock {
-
-    /** @return the node of this block */
-    Node getNode();
-
-    /** @return the list of exceptional successor blocks as an unmodifiable map */
-    Map<TypeMirror, Set<Block>> getExceptionalSuccessors();
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ExceptionBlockImpl.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ExceptionBlockImpl.java
deleted file mode 100644
index 2a6c3b4914..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/ExceptionBlockImpl.java
+++ /dev/null
@@ -1,66 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-import java.util.Collections;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Map;
-import java.util.Set;
-import javax.lang.model.type.TypeMirror;
-import org.checkerframework.dataflow.cfg.node.Node;
-
-/**
- * Base class of the {@link Block} implementation hierarchy.
- *
- * @author Stefan Heule
- */
-public class ExceptionBlockImpl extends SingleSuccessorBlockImpl implements ExceptionBlock {
-
-    /** Set of exceptional successors. */
-    protected Map<TypeMirror, Set<Block>> exceptionalSuccessors;
-
-    public ExceptionBlockImpl() {
-        type = BlockType.EXCEPTION_BLOCK;
-        exceptionalSuccessors = new HashMap<>();
-    }
-
-    /** The node of this block. */
-    protected Node node;
-
-    /** Set the node. */
-    public void setNode(Node c) {
-        node = c;
-        c.setBlock(this);
-    }
-
-    @Override
-    public Node getNode() {
-        return node;
-    }
-
-    /** Add an exceptional successor. */
-    public void addExceptionalSuccessor(BlockImpl b, TypeMirror cause) {
-        if (exceptionalSuccessors == null) {
-            exceptionalSuccessors = new HashMap<>();
-        }
-        Set<Block> blocks = exceptionalSuccessors.get(cause);
-        if (blocks == null) {
-            blocks = new HashSet<Block>();
-            exceptionalSuccessors.put(cause, blocks);
-        }
-        blocks.add(b);
-        b.addPredecessor(this);
-    }
-
-    @Override
-    public Map<TypeMirror, Set<Block>> getExceptionalSuccessors() {
-        if (exceptionalSuccessors == null) {
-            return Collections.emptyMap();
-        }
-        return Collections.unmodifiableMap(exceptionalSuccessors);
-    }
-
-    @Override
-    public String toString() {
-        return "ExceptionBlock(" + node + ")";
-    }
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/RegularBlock.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/RegularBlock.java
deleted file mode 100644
index 566449257b..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/RegularBlock.java
+++ /dev/null
@@ -1,27 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-import java.util.List;
-import org.checkerframework.dataflow.cfg.node.Node;
-
-/**
- * A regular basic block that contains a sequence of {@link Node}s.
- *
- * <p>The following invariant holds.
- *
- * <pre>
- * forall n in getContents() :: n.getBlock() == this
- * </pre>
- *
- * @author Stefan Heule
- */
-public interface RegularBlock extends SingleSuccessorBlock {
-
-    /** @return the unmodifiable sequence of {@link Node}s. */
-    List<Node> getContents();
-
-    /** @return the regular successor block */
-    Block getRegularSuccessor();
-
-    /** Is this block empty (i.e., does it not contain any contents). */
-    boolean isEmpty();
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/RegularBlockImpl.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/RegularBlockImpl.java
deleted file mode 100644
index b302710d70..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/RegularBlockImpl.java
+++ /dev/null
@@ -1,59 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-import java.util.Collections;
-import java.util.LinkedList;
-import java.util.List;
-import org.checkerframework.dataflow.cfg.node.Node;
-
-/**
- * Implementation of a regular basic block.
- *
- * @author Stefan Heule
- */
-public class RegularBlockImpl extends SingleSuccessorBlockImpl implements RegularBlock {
-
-    /** Internal representation of the contents. */
-    protected List<Node> contents;
-
-    /**
-     * Initialize an empty basic block to be filled with contents and linked to other basic blocks
-     * later.
-     */
-    public RegularBlockImpl() {
-        contents = new LinkedList<>();
-        type = BlockType.REGULAR_BLOCK;
-    }
-
-    /** Add a node to the contents of this basic block. */
-    public void addNode(Node t) {
-        contents.add(t);
-        t.setBlock(this);
-    }
-
-    /** Add multiple nodes to the contents of this basic block. */
-    public void addNodes(List<? extends Node> ts) {
-        for (Node t : ts) {
-            addNode(t);
-        }
-    }
-
-    @Override
-    public List<Node> getContents() {
-        return Collections.unmodifiableList(contents);
-    }
-
-    @Override
-    public BlockImpl getRegularSuccessor() {
-        return successor;
-    }
-
-    @Override
-    public String toString() {
-        return "RegularBlock(" + contents + ")";
-    }
-
-    @Override
-    public boolean isEmpty() {
-        return contents.isEmpty();
-    }
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlock.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlock.java
deleted file mode 100644
index 038a69d3e4..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlock.java
+++ /dev/null
@@ -1,24 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-/*>>>
-import org.checkerframework.checker.nullness.qual.Nullable;
-*/
-
-import org.checkerframework.dataflow.analysis.Store;
-
-/**
- * A basic block that has at exactly one non-exceptional successor.
- *
- * @author Stefan Heule
- */
-public interface SingleSuccessorBlock extends Block {
-
-    /** @return the non-exceptional successor block, or {@code null} if there is no successor. */
-    /*@Nullable*/ Block getSuccessor();
-
-    /** @return the flow rule for information flowing from this block to its successor */
-    Store.FlowRule getFlowRule();
-
-    /** Set the flow rule for information flowing from this block to its successor. */
-    void setFlowRule(Store.FlowRule rule);
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java
deleted file mode 100644
index 9e8872e850..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java
+++ /dev/null
@@ -1,45 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-/*>>>
-import org.checkerframework.checker.nullness.qual.Nullable;
-*/
-
-import org.checkerframework.dataflow.analysis.Store;
-
-/**
- * Implementation of a non-special basic block.
- *
- * @author Stefan Heule
- */
-public abstract class SingleSuccessorBlockImpl extends BlockImpl implements SingleSuccessorBlock {
-
-    /** Internal representation of the successor. */
-    protected /*@Nullable*/ BlockImpl successor;
-
-    /**
-     * The rule below say that EACH store at the end of a single successor block flow to the
-     * corresponding store of the successor.
-     */
-    protected Store.FlowRule flowRule = Store.FlowRule.EACH_TO_EACH;
-
-    @Override
-    public /*@Nullable*/ Block getSuccessor() {
-        return successor;
-    }
-
-    /** Set a basic block as the successor of this block. */
-    public void setSuccessor(BlockImpl successor) {
-        this.successor = successor;
-        successor.addPredecessor(this);
-    }
-
-    @Override
-    public Store.FlowRule getFlowRule() {
-        return flowRule;
-    }
-
-    @Override
-    public void setFlowRule(Store.FlowRule rule) {
-        flowRule = rule;
-    }
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SpecialBlock.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SpecialBlock.java
deleted file mode 100644
index dac9b4b8c2..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SpecialBlock.java
+++ /dev/null
@@ -1,31 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-/**
- * Represents a special basic block; i.e., one of the following:
- *
- * <ul>
- *   <li>Entry block of a method.
- *   <li>Regular exit block of a method.
- *   <li>Exceptional exit block of a method.
- * </ul>
- *
- * @author Stefan Heule
- */
-public interface SpecialBlock extends SingleSuccessorBlock {
-
-    /** The types of special basic blocks */
-    public static enum SpecialBlockType {
-
-        /** The entry block of a method */
-        ENTRY,
-
-        /** The exit block of a method */
-        EXIT,
-
-        /** A special exit block of a method for exceptional termination */
-        EXCEPTIONAL_EXIT,
-    }
-
-    /** @return the type of this special basic block */
-    SpecialBlockType getSpecialType();
-}
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SpecialBlockImpl.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SpecialBlockImpl.java
deleted file mode 100644
index e6f25e8b1b..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/cfg/block/SpecialBlockImpl.java
+++ /dev/null
@@ -1,22 +0,0 @@
-package org.checkerframework.dataflow.cfg.block;
-
-public class SpecialBlockImpl extends SingleSuccessorBlockImpl implements SpecialBlock {
-
-    /** The type of this special basic block. */
-    protected SpecialBlockType specialType;
-
-    public SpecialBlockImpl(SpecialBlockType type) {
-        this.specialType = type;
-        this.type = BlockType.SPECIAL_BLOCK;
-    }
-
-    @Override
-    public SpecialBlockType getSpecialType() {
-        return specialType;
-    }
-
-    @Override
-    public String toString() {
-        return "SpecialBlock(" + specialType + ")";
-    }
-}