diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ConditionalBlock.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ConditionalBlock.java index 3570d36399e..334b8f1ffce 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ConditionalBlock.java +++ b/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); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ConditionalBlockImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ConditionalBlockImpl.java index 3f748b136e2..6cdbcff0aef 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/ConditionalBlockImpl.java +++ b/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 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; } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlock.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlock.java index a5d1ac9281e..b626e1d6092 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlock.java +++ b/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); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java index 83a909ef4c5..0b59a01c9dd 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/block/SingleSuccessorBlockImpl.java +++ b/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; } } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 0d3ca49379e..fe682c31539 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/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); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ConditionalJump.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ConditionalJump.java index ab95b200414..03e28a98ab8 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ConditionalJump.java +++ b/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; } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/MissingEdge.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/MissingEdge.java index c17d935a61e..3d7884a1670 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/MissingEdge.java +++ b/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; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/UnconditionalJump.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/UnconditionalJump.java index 3be91aa74bd..0a131bf1ff7 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/UnconditionalJump.java +++ b/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,7 +10,7 @@ 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. @@ -18,7 +18,7 @@ class UnconditionalJump extends ExtendedNode { * @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; }