Import Store.FlowRule (#3836)

dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ConditionalBlock.java

@@ -1,6 +1,6 @@
 package org.checkerframework.dataflow.cfg.block;
 
-import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.analysis.Store.FlowRule;
 
 // Werner believes that a ConditionalBlock has to have exactly one RegularBlock (?) predecessor and
 // the last node of that predecessor has to be a node of boolean type. He's not totally sure,
@@ -28,18 +28,26 @@ public interface ConditionalBlock extends Block {
      *
      * @return the flow rule for information flowing from this block to its then successor
      */
-    Store.FlowRule getThenFlowRule();
+    FlowRule getThenFlowRule();
 
     /**
      * Returns the flow rule for information flowing from this block to its else successor.
      *
      * @return the flow rule for information flowing from this block to its else successor
      */
-    Store.FlowRule getElseFlowRule();
+    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 then successor.
+     *
+     * @param rule the new flow rule for information flowing from this block to its then successor
+     */
+    void setThenFlowRule(FlowRule rule);
 
-    /** Set the flow rule for information flowing from this block to its else successor. */
-    void setElseFlowRule(Store.FlowRule rule);
+    /**
+     * Set the flow rule for information flowing from this block to its else successor.
+     *
+     * @param rule the new flow rule for information flowing from this block to its else successor
+     */
+    void setElseFlowRule(FlowRule rule);
 }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ConditionalBlockImpl.java

@@ -5,7 +5,7 @@
 import java.util.List;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.analysis.Store.FlowRule;
 import org.checkerframework.dataflow.cfg.node.Node;
 import org.checkerframework.javacutil.BugInCF;
 
@@ -19,13 +19,16 @@ public class ConditionalBlockImpl extends BlockImpl implements ConditionalBlock
     protected @Nullable BlockImpl elseSuccessor;
 
     /**
-     * The initial values for 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.
+     * The initial value says that the THEN store before a conditional block flows to BOTH of the
+     * stores of the then successor.
      */
-    protected Store.FlowRule thenFlowRule = Store.FlowRule.THEN_TO_BOTH;
+    protected FlowRule thenFlowRule = FlowRule.THEN_TO_BOTH;
 
-    protected Store.FlowRule elseFlowRule = Store.FlowRule.ELSE_TO_BOTH;
+    /**
+     * The initial value says that the ELSE store before a conditional block flows to BOTH of the
+     * stores of the else successor.
+     */
+    protected FlowRule elseFlowRule = FlowRule.ELSE_TO_BOTH;
 
     /**
      * Initialize an empty conditional basic block to be filled with contents and linked to other
@@ -74,22 +77,22 @@ public Set<Block> getSuccessors() {
     }
 
     @Override
-    public Store.FlowRule getThenFlowRule() {
+    public FlowRule getThenFlowRule() {
         return thenFlowRule;
     }
 
     @Override
-    public Store.FlowRule getElseFlowRule() {
+    public FlowRule getElseFlowRule() {
         return elseFlowRule;
     }
 
     @Override
-    public void setThenFlowRule(Store.FlowRule rule) {
+    public void setThenFlowRule(FlowRule rule) {
         thenFlowRule = rule;
     }
 
     @Override
-    public void setElseFlowRule(Store.FlowRule rule) {
+    public void setElseFlowRule(FlowRule rule) {
         elseFlowRule = rule;
     }
 

dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlock.java

@@ -1,7 +1,7 @@
 package org.checkerframework.dataflow.cfg.block;
 
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.analysis.Store.FlowRule;
 import org.checkerframework.dataflow.qual.Pure;
 
 /** A basic block that has at exactly one non-exceptional successor. */
@@ -23,8 +23,12 @@ public interface SingleSuccessorBlock extends Block {
      * @return the flow rule for information flowing from this block to its successor
      */
     @Pure
-    Store.FlowRule getFlowRule();
+    FlowRule getFlowRule();
 
-    /** Set the flow rule for information flowing from this block to its successor. */
-    void setFlowRule(Store.FlowRule rule);
+    /**
+     * Set the flow rule for information flowing from this block to its successor.
+     *
+     * @param rule the new flow rule for information flowing from this block to its successor
+     */
+    void setFlowRule(FlowRule rule);
 }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java

@@ -3,7 +3,7 @@
 import java.util.LinkedHashSet;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.analysis.Store.FlowRule;
 
 /**
  * A basic block that has at most one successor. SpecialBlockImpl extends this, but exit blocks have
@@ -18,8 +18,13 @@ public abstract class SingleSuccessorBlockImpl extends BlockImpl implements Sing
      * The initial value for the rule below says that EACH store at the end of a single successor
      * block flows to the corresponding store of the successor.
      */
-    protected Store.FlowRule flowRule = Store.FlowRule.EACH_TO_EACH;
+    protected FlowRule flowRule = FlowRule.EACH_TO_EACH;
 
+    /**
+     * Creates a new SingleSuccessorBlock.
+     *
+     * @param type the type of this basic block
+     */
     protected SingleSuccessorBlockImpl(BlockType type) {
         super(type);
     }
@@ -49,12 +54,12 @@ public void setSuccessor(BlockImpl successor) {
     }
 
     @Override
-    public Store.FlowRule getFlowRule() {
+    public FlowRule getFlowRule() {
         return flowRule;
     }
 
     @Override
-    public void setFlowRule(Store.FlowRule rule) {
+    public void setFlowRule(FlowRule rule) {
         flowRule = rule;
     }
 }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java

@@ -89,7 +89,7 @@
 import javax.lang.model.util.Types;
 import org.checkerframework.checker.interning.qual.FindDistinct;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.analysis.Store.FlowRule;
 import org.checkerframework.dataflow.cfg.UnderlyingAST;
 import org.checkerframework.dataflow.cfg.node.ArrayAccessNode;
 import org.checkerframework.dataflow.cfg.node.ArrayCreationNode;
@@ -1989,10 +1989,10 @@ public Node visitBinary(BinaryTree tree, Void p) {
                     ConditionalJump cjump;
                     if (kind == Tree.Kind.CONDITIONAL_AND) {
                         cjump = new ConditionalJump(rightStartL, shortCircuitL);
-                        cjump.setFalseFlowRule(Store.FlowRule.ELSE_TO_ELSE);
+                        cjump.setFalseFlowRule(FlowRule.ELSE_TO_ELSE);
                     } else {
                         cjump = new ConditionalJump(shortCircuitL, rightStartL);
-                        cjump.setTrueFlowRule(Store.FlowRule.THEN_TO_THEN);
+                        cjump.setTrueFlowRule(FlowRule.THEN_TO_THEN);
                     }
                     extendWithExtendedNode(cjump);
 
@@ -2196,12 +2196,12 @@ public Node visitConditionalExpression(ConditionalExpressionTree tree, Void p) {
         addLabelForNextNode(trueStart);
         Node trueExpr = scan(tree.getTrueExpression(), p);
         trueExpr = conditionalExprPromotion(trueExpr, exprType);
-        extendWithExtendedNode(new UnconditionalJump(merge, Store.FlowRule.BOTH_TO_THEN));
+        extendWithExtendedNode(new UnconditionalJump(merge, FlowRule.BOTH_TO_THEN));
 
         addLabelForNextNode(falseStart);
         Node falseExpr = scan(tree.getFalseExpression(), p);
         falseExpr = conditionalExprPromotion(falseExpr, exprType);
-        extendWithExtendedNode(new UnconditionalJump(merge, Store.FlowRule.BOTH_TO_ELSE));
+        extendWithExtendedNode(new UnconditionalJump(merge, FlowRule.BOTH_TO_ELSE));
 
         addLabelForNextNode(merge);
         Node node = new TernaryExpressionNode(tree, condition, trueExpr, falseExpr);

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ConditionalJump.java

@@ -1,6 +1,6 @@
 package org.checkerframework.dataflow.cfg.builder;
 
-import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.analysis.Store.FlowRule;
 import org.checkerframework.dataflow.cfg.builder.ExtendedNode.ExtendedNodeType;
 
 /**
@@ -20,9 +20,9 @@ class ConditionalJump extends ExtendedNode {
     protected final Label falseSucc;
 
     /** The true branch flow rule. */
-    protected Store.FlowRule trueFlowRule;
+    protected FlowRule trueFlowRule;
     /** The false branch flow rule. */
-    protected Store.FlowRule falseFlowRule;
+    protected FlowRule falseFlowRule;
 
     /**
      * Construct a ConditionalJump.
@@ -46,19 +46,39 @@ public Label getElseLabel() {
         return falseSucc;
     }
 
-    public Store.FlowRule getTrueFlowRule() {
+    /**
+     * Returns the true branch flow rule.
+     *
+     * @return the true branch flow rule
+     */
+    public FlowRule getTrueFlowRule() {
         return trueFlowRule;
     }
 
-    public Store.FlowRule getFalseFlowRule() {
+    /**
+     * Returns the false branch flow rule.
+     *
+     * @return the false branch flow rule
+     */
+    public FlowRule getFalseFlowRule() {
         return falseFlowRule;
     }
 
-    public void setTrueFlowRule(Store.FlowRule rule) {
+    /**
+     * Sets the true branch flow rule.
+     *
+     * @param rule the new true branch flow rule
+     */
+    public void setTrueFlowRule(FlowRule rule) {
         trueFlowRule = rule;
     }
 
-    public void setFalseFlowRule(Store.FlowRule rule) {
+    /**
+     * Sets the false branch flow rule.
+     *
+     * @param rule the new false branch flow rule
+     */
+    public void setFalseFlowRule(FlowRule rule) {
         falseFlowRule = rule;
     }
 

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/MissingEdge.java

@@ -2,7 +2,7 @@
 
 import javax.lang.model.type.TypeMirror;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.analysis.Store.FlowRule;
 import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlockImpl;
 
 /* --------------------------------------------------------- */
@@ -19,7 +19,7 @@ class MissingEdge {
     final @Nullable TypeMirror cause;
 
     /** The flow rule for this edge. */
-    final Store.@Nullable FlowRule flowRule;
+    final @Nullable FlowRule flowRule;
 
     /**
      * Create a new MissingEdge.
@@ -28,7 +28,7 @@ class MissingEdge {
      * @param index the index (target?) of the edge
      */
     public MissingEdge(SingleSuccessorBlockImpl source, int index) {
-        this(source, index, null, Store.FlowRule.EACH_TO_EACH);
+        this(source, index, null, FlowRule.EACH_TO_EACH);
     }
 
     /**
@@ -38,7 +38,7 @@ public MissingEdge(SingleSuccessorBlockImpl source, int index) {
      * @param index the index (target?) of the edge
      * @param flowRule the flow rule for this edge
      */
-    public MissingEdge(SingleSuccessorBlockImpl source, int index, Store.FlowRule flowRule) {
+    public MissingEdge(SingleSuccessorBlockImpl source, int index, FlowRule flowRule) {
         this(source, index, null, flowRule);
     }
 
@@ -51,7 +51,7 @@ public MissingEdge(SingleSuccessorBlockImpl source, int index, Store.FlowRule fl
      */
     public MissingEdge(
             SingleSuccessorBlockImpl source, @Nullable Integer index, @Nullable TypeMirror cause) {
-        this(source, index, cause, Store.FlowRule.EACH_TO_EACH);
+        this(source, index, cause, FlowRule.EACH_TO_EACH);
     }
 
     /**
@@ -66,7 +66,7 @@ public MissingEdge(
             SingleSuccessorBlockImpl source,
             @Nullable Integer index,
             @Nullable TypeMirror cause,
-            Store.FlowRule flowRule) {
+            FlowRule flowRule) {
         assert (index != null) || (cause != null);
         this.source = source;
         this.index = index;

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/UnconditionalJump.java

@@ -1,6 +1,6 @@
 package org.checkerframework.dataflow.cfg.builder;
 
-import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.analysis.Store.FlowRule;
 import org.checkerframework.dataflow.cfg.builder.ExtendedNode.ExtendedNodeType;
 
 /** An extended node of type {@link ExtendedNodeType#UNCONDITIONAL_JUMP}. */
@@ -10,15 +10,15 @@ class UnconditionalJump extends ExtendedNode {
     protected final Label jumpTarget;
 
     /** The flow rule for this edge. */
-    protected final Store.FlowRule flowRule;
+    protected final FlowRule flowRule;
 
     /**
      * Construct an UnconditionalJump.
      *
      * @param jumpTarget the jump target label
      */
     public UnconditionalJump(Label jumpTarget) {
-        this(jumpTarget, Store.FlowRule.EACH_TO_EACH);
+        this(jumpTarget, FlowRule.EACH_TO_EACH);
     }
 
     /**
@@ -27,7 +27,7 @@ public UnconditionalJump(Label jumpTarget) {
      * @param jumpTarget the jump target label
      * @param flowRule the flow rule for this edge
      */
-    public UnconditionalJump(Label jumpTarget, Store.FlowRule flowRule) {
+    public UnconditionalJump(Label jumpTarget, FlowRule flowRule) {
         super(ExtendedNodeType.UNCONDITIONAL_JUMP);
         assert jumpTarget != null;
         this.jumpTarget = jumpTarget;
@@ -44,7 +44,7 @@ public Label getLabel() {
      *
      * @return the flow rule for this edge
      */
-    public Store.FlowRule getFlowRule() {
+    public FlowRule getFlowRule() {
         return flowRule;
     }