aboutsummaryrefslogtreecommitdiffhomepage
path: root/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Analysis.java
diff options
context:
space:
mode:
Diffstat (limited to 'third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Analysis.java')
-rw-r--r--third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Analysis.java649
1 files changed, 348 insertions, 301 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Analysis.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Analysis.java
index fa07247e68..2e81b4af4a 100644
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Analysis.java
+++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Analysis.java
@@ -4,7 +4,25 @@ package org.checkerframework.dataflow.analysis;
import org.checkerframework.checker.nullness.qual.Nullable;
*/
+import com.sun.source.tree.ClassTree;
import com.sun.source.tree.LambdaExpressionTree;
+import com.sun.source.tree.MethodTree;
+import com.sun.source.tree.Tree;
+import com.sun.source.tree.VariableTree;
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.IdentityHashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Objects;
+import java.util.PriorityQueue;
+import java.util.Set;
+import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.element.Element;
+import javax.lang.model.type.TypeMirror;
+import javax.lang.model.util.Types;
import org.checkerframework.dataflow.cfg.ControlFlowGraph;
import org.checkerframework.dataflow.cfg.UnderlyingAST;
import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda;
@@ -19,46 +37,20 @@ import org.checkerframework.dataflow.cfg.node.AssignmentNode;
import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.dataflow.cfg.node.Node;
import org.checkerframework.dataflow.cfg.node.ReturnNode;
-
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.Pair;
-import java.util.ArrayList;
-import java.util.Comparator;
-import java.util.HashMap;
-import java.util.IdentityHashMap;
-import java.util.List;
-import java.util.Map;
-import java.util.Map.Entry;
-import java.util.Objects;
-import java.util.PriorityQueue;
-import java.util.Set;
-
-import javax.annotation.processing.ProcessingEnvironment;
-import javax.lang.model.element.Element;
-import javax.lang.model.type.TypeMirror;
-import javax.lang.model.util.Types;
-
-import com.sun.source.tree.ClassTree;
-import com.sun.source.tree.MethodTree;
-import com.sun.source.tree.Tree;
-import com.sun.source.tree.VariableTree;
-
/**
* An implementation of an iterative algorithm to solve a org.checkerframework.dataflow problem,
* given a control flow graph and a transfer function.
*
* @author Stefan Heule
- *
- * @param <A>
- * The abstract value type to be tracked by the analysis.
- * @param <S>
- * The store type used in the analysis.
- * @param <T>
- * The transfer function type that is used to approximated runtime
- * behavior.
+ * @param <A> the abstract value type to be tracked by the analysis
+ * @param <S> the store type used in the analysis
+ * @param <T> the transfer function type that is used to approximated runtime behavior
*/
-public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends TransferFunction<A, S>> {
+public class Analysis<
+ A extends AbstractValue<A>, S extends Store<S>, T extends TransferFunction<A, S>> {
/** Is the analysis currently running? */
protected boolean isRunning = false;
@@ -75,27 +67,30 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
/** Instance of the types utility. */
protected final Types types;
- /**
- * Then stores before every basic block (assumed to be 'no information' if
- * not present).
- */
+ /** Then stores before every basic block (assumed to be 'no information' if not present). */
protected IdentityHashMap<Block, S> thenStores;
+ /** Else stores before every basic block (assumed to be 'no information' if not present). */
+ protected IdentityHashMap<Block, S> elseStores;
+
/**
- * Else stores before every basic block (assumed to be 'no information' if
- * not present).
+ * Number of times every block has been analyzed since the last time widening was applied. Null,
+ * if maxCountBeforeWidening is -1 which implies widening isn't used for this analysis.
*/
- protected IdentityHashMap<Block, S> elseStores;
+ protected IdentityHashMap<Block, Integer> blockCount;
/**
- * The transfer inputs before every basic block (assumed to be 'no information' if
- * not present).
+ * Number of times a block can be analyzed before widening. -1 implies that widening shouldn't
+ * be used.
*/
- protected IdentityHashMap<Block, TransferInput<A, S>> inputs;
+ protected final int maxCountBeforeWidening;
/**
- * The stores after every return statement.
+ * The transfer inputs before every basic block (assumed to be 'no information' if not present).
*/
+ protected IdentityHashMap<Block, TransferInput<A, S>> inputs;
+
+ /** The stores after every return statement. */
protected IdentityHashMap<ReturnNode, TransferResult<A, S>> storesAtReturnStatements;
/** The worklist used for the fix-point iteration. */
@@ -108,25 +103,22 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
public HashMap<Element, A> finalLocalValues;
/**
- * The node that is currently handled in the analysis (if it is running).
- * The following invariant holds:
+ * The node that is currently handled in the analysis (if it is running). The following
+ * invariant holds:
*
* <pre>
- * !isRunning ==&gt; (currentNode == null)
+ * !isRunning &rArr; (currentNode == null)
* </pre>
*/
protected Node currentNode;
/**
- * The tree that is currently being looked at. The transfer function can set
- * this tree to make sure that calls to {@code getValue} will not return
- * information for this given tree.
+ * The tree that is currently being looked at. The transfer function can set this tree to make
+ * sure that calls to {@code getValue} will not return information for this given tree.
*/
protected Tree currentTree;
- /**
- * The current transfer input when the analysis is running.
- */
+ /** The current transfer input when the analysis is running. */
protected TransferInput<A, S> currentInput;
public Tree getCurrentTree() {
@@ -139,12 +131,10 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
/**
* Construct an object that can perform a org.checkerframework.dataflow analysis over a control
- * flow graph. The transfer function is set later using
- * {@code setTransferFunction}.
+ * flow graph. The transfer function is set later using {@code setTransferFunction}.
*/
public Analysis(ProcessingEnvironment env) {
- this.env = env;
- types = env.getTypeUtils();
+ this(env, null, -1);
}
/**
@@ -152,7 +142,18 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
* flow graph, given a transfer function.
*/
public Analysis(ProcessingEnvironment env, T transfer) {
- this(env);
+ this(env, transfer, -1);
+ }
+
+ /**
+ * Construct an object that can perform a org.checkerframework.dataflow analysis over a control
+ * flow graph, given a transfer function.
+ */
+ public Analysis(ProcessingEnvironment env, T transfer, int maxCountBeforeWidening) {
+ this.env = env;
+ types = env.getTypeUtils();
+ this.transferFunction = transfer;
+ this.maxCountBeforeWidening = maxCountBeforeWidening;
this.transferFunction = transfer;
}
@@ -173,10 +174,7 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
/**
- * Perform the actual analysis. Should only be called once after the object
- * has been created.
- *
- * @param cfg
+ * Perform the actual analysis. Should only be called once after the object has been created.
*/
public void performAnalysis(ControlFlowGraph cfg) {
assert isRunning == false;
@@ -188,101 +186,116 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
Block b = worklist.poll();
switch (b.getType()) {
- case REGULAR_BLOCK: {
- RegularBlock rb = (RegularBlock) b;
-
- // apply transfer function to contents
- TransferInput<A, S> inputBefore = getInputBefore(rb);
- currentInput = inputBefore.copy();
- TransferResult<A, S> transferResult = null;
- Node lastNode = null;
- boolean addToWorklistAgain = false;
- for (Node n : rb.getContents()) {
- transferResult = callTransferFunction(n, currentInput);
- addToWorklistAgain |= updateNodeValues(n, transferResult);
- currentInput = new TransferInput<>(n, this, transferResult);
- lastNode = n;
- }
- // loop will run at least one, making transferResult non-null
-
- // propagate store to successors
- Block succ = rb.getSuccessor();
- assert succ != null : "regular basic block without non-exceptional successor unexpected";
- propagateStoresTo(succ, lastNode, currentInput, rb.getFlowRule(), addToWorklistAgain);
- break;
- }
-
- case EXCEPTION_BLOCK: {
- ExceptionBlock eb = (ExceptionBlock) b;
-
- // apply transfer function to content
- TransferInput<A, S> inputBefore = getInputBefore(eb);
- currentInput = inputBefore.copy();
- Node node = eb.getNode();
- TransferResult<A, S> transferResult = callTransferFunction(
- node, currentInput);
- boolean addToWorklistAgain = updateNodeValues(node, transferResult);
-
- // propagate store to successor
- Block succ = eb.getSuccessor();
- if (succ != null) {
- currentInput = new TransferInput<>(node, this, transferResult);
- // TODO? Variable wasn't used.
- // Store.FlowRule storeFlow = eb.getFlowRule();
- propagateStoresTo(succ, node, currentInput, eb.getFlowRule(), addToWorklistAgain);
- }
+ case REGULAR_BLOCK:
+ {
+ RegularBlock rb = (RegularBlock) b;
+
+ // apply transfer function to contents
+ TransferInput<A, S> inputBefore = getInputBefore(rb);
+ currentInput = inputBefore.copy();
+ TransferResult<A, S> transferResult = null;
+ Node lastNode = null;
+ boolean addToWorklistAgain = false;
+ for (Node n : rb.getContents()) {
+ transferResult = callTransferFunction(n, currentInput);
+ addToWorklistAgain |= updateNodeValues(n, transferResult);
+ currentInput = new TransferInput<>(n, this, transferResult);
+ lastNode = n;
+ }
+ // loop will run at least one, making transferResult non-null
+
+ // propagate store to successors
+ Block succ = rb.getSuccessor();
+ assert succ != null
+ : "regular basic block without non-exceptional successor unexpected";
+ propagateStoresTo(
+ succ, lastNode, currentInput, rb.getFlowRule(), addToWorklistAgain);
+ break;
+ }
- // propagate store to exceptional successors
- for (Entry<TypeMirror, Set<Block>> e : eb.getExceptionalSuccessors()
- .entrySet()) {
- TypeMirror cause = e.getKey();
- S exceptionalStore = transferResult
- .getExceptionalStore(cause);
- if (exceptionalStore != null) {
- for (Block exceptionSucc : e.getValue()) {
- addStoreBefore(exceptionSucc, node, exceptionalStore, Store.Kind.BOTH,
- addToWorklistAgain);
+ case EXCEPTION_BLOCK:
+ {
+ ExceptionBlock eb = (ExceptionBlock) b;
+
+ // apply transfer function to content
+ TransferInput<A, S> inputBefore = getInputBefore(eb);
+ currentInput = inputBefore.copy();
+ Node node = eb.getNode();
+ TransferResult<A, S> transferResult =
+ callTransferFunction(node, currentInput);
+ boolean addToWorklistAgain = updateNodeValues(node, transferResult);
+
+ // propagate store to successor
+ Block succ = eb.getSuccessor();
+ if (succ != null) {
+ currentInput = new TransferInput<>(node, this, transferResult);
+ // TODO? Variable wasn't used.
+ // Store.FlowRule storeFlow = eb.getFlowRule();
+ propagateStoresTo(
+ succ, node, currentInput, eb.getFlowRule(), addToWorklistAgain);
}
- } else {
- for (Block exceptionSucc : e.getValue()) {
- addStoreBefore(exceptionSucc, node, inputBefore.copy().getRegularStore(),
- Store.Kind.BOTH, addToWorklistAgain);
+
+ // propagate store to exceptional successors
+ for (Entry<TypeMirror, Set<Block>> e :
+ eb.getExceptionalSuccessors().entrySet()) {
+ TypeMirror cause = e.getKey();
+ S exceptionalStore = transferResult.getExceptionalStore(cause);
+ if (exceptionalStore != null) {
+ for (Block exceptionSucc : e.getValue()) {
+ addStoreBefore(
+ exceptionSucc,
+ node,
+ exceptionalStore,
+ Store.Kind.BOTH,
+ addToWorklistAgain);
+ }
+ } else {
+ for (Block exceptionSucc : e.getValue()) {
+ addStoreBefore(
+ exceptionSucc,
+ node,
+ inputBefore.copy().getRegularStore(),
+ Store.Kind.BOTH,
+ addToWorklistAgain);
+ }
+ }
}
+ break;
}
- }
- break;
- }
- case CONDITIONAL_BLOCK: {
- ConditionalBlock cb = (ConditionalBlock) b;
+ case CONDITIONAL_BLOCK:
+ {
+ ConditionalBlock cb = (ConditionalBlock) b;
- // get store before
- TransferInput<A, S> inputBefore = getInputBefore(cb);
- TransferInput<A, S> input = inputBefore.copy();
+ // get store before
+ TransferInput<A, S> inputBefore = getInputBefore(cb);
+ TransferInput<A, S> input = inputBefore.copy();
- // propagate store to successor
- Block thenSucc = cb.getThenSuccessor();
- Block elseSucc = cb.getElseSuccessor();
+ // propagate store to successor
+ Block thenSucc = cb.getThenSuccessor();
+ Block elseSucc = cb.getElseSuccessor();
- propagateStoresTo(thenSucc, null, input, cb.getThenFlowRule(), false);
- propagateStoresTo(elseSucc, null, input, cb.getElseFlowRule(), false);
- break;
- }
+ propagateStoresTo(thenSucc, null, input, cb.getThenFlowRule(), false);
+ propagateStoresTo(elseSucc, null, input, cb.getElseFlowRule(), false);
+ break;
+ }
- case SPECIAL_BLOCK: {
- // special basic blocks are empty and cannot throw exceptions,
- // thus there is no need to perform any analysis.
- SpecialBlock sb = (SpecialBlock) b;
- Block succ = sb.getSuccessor();
- if (succ != null) {
- propagateStoresTo(succ, null, getInputBefore(b), sb.getFlowRule(), false);
- }
- break;
- }
+ case SPECIAL_BLOCK:
+ {
+ // special basic blocks are empty and cannot throw exceptions,
+ // thus there is no need to perform any analysis.
+ SpecialBlock sb = (SpecialBlock) b;
+ Block succ = sb.getSuccessor();
+ if (succ != null) {
+ propagateStoresTo(
+ succ, null, getInputBefore(b), sb.getFlowRule(), false);
+ }
+ break;
+ }
- default:
- assert false;
- break;
+ default:
+ assert false;
+ break;
}
}
@@ -291,78 +304,104 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
/**
- * Propagate the stores in currentInput to the successor block, succ, according to the
- * flowRule.
+ * Propagate the stores in currentInput to the successor block, succ, according to the flowRule.
*/
- protected void propagateStoresTo(Block succ, Node node, TransferInput<A, S> currentInput,
- Store.FlowRule flowRule, boolean addToWorklistAgain) {
+ protected void propagateStoresTo(
+ Block succ,
+ Node node,
+ TransferInput<A, S> currentInput,
+ Store.FlowRule flowRule,
+ boolean addToWorklistAgain) {
switch (flowRule) {
- case EACH_TO_EACH:
- if (currentInput.containsTwoStores()) {
- addStoreBefore(succ, node, currentInput.getThenStore(), Store.Kind.THEN,
+ case EACH_TO_EACH:
+ if (currentInput.containsTwoStores()) {
+ addStoreBefore(
+ succ,
+ node,
+ currentInput.getThenStore(),
+ Store.Kind.THEN,
+ addToWorklistAgain);
+ addStoreBefore(
+ succ,
+ node,
+ currentInput.getElseStore(),
+ Store.Kind.ELSE,
+ addToWorklistAgain);
+ } else {
+ addStoreBefore(
+ succ,
+ node,
+ currentInput.getRegularStore(),
+ Store.Kind.BOTH,
+ addToWorklistAgain);
+ }
+ break;
+ case THEN_TO_BOTH:
+ addStoreBefore(
+ succ,
+ node,
+ currentInput.getThenStore(),
+ Store.Kind.BOTH,
addToWorklistAgain);
- addStoreBefore(succ, node, currentInput.getElseStore(), Store.Kind.ELSE,
+ break;
+ case ELSE_TO_BOTH:
+ addStoreBefore(
+ succ,
+ node,
+ currentInput.getElseStore(),
+ Store.Kind.BOTH,
addToWorklistAgain);
- } else {
- addStoreBefore(succ, node, currentInput.getRegularStore(), Store.Kind.BOTH,
+ break;
+ case THEN_TO_THEN:
+ addStoreBefore(
+ succ,
+ node,
+ currentInput.getThenStore(),
+ Store.Kind.THEN,
addToWorklistAgain);
- }
- break;
- case THEN_TO_BOTH:
- addStoreBefore(succ, node, currentInput.getThenStore(), Store.Kind.BOTH,
- addToWorklistAgain);
- break;
- case ELSE_TO_BOTH:
- addStoreBefore(succ, node, currentInput.getElseStore(), Store.Kind.BOTH,
- addToWorklistAgain);
- break;
- case THEN_TO_THEN:
- addStoreBefore(succ, node, currentInput.getThenStore(), Store.Kind.THEN,
- addToWorklistAgain);
- break;
- case ELSE_TO_ELSE:
- addStoreBefore(succ, node, currentInput.getElseStore(), Store.Kind.ELSE,
- addToWorklistAgain);
- break;
+ break;
+ case ELSE_TO_ELSE:
+ addStoreBefore(
+ succ,
+ node,
+ currentInput.getElseStore(),
+ Store.Kind.ELSE,
+ addToWorklistAgain);
+ break;
}
}
/**
- * Updates the value of node {@code node} to the value of the
- * {@code transferResult}. Returns true if the node's value changed, or a
- * store was updated.
+ * Updates the value of node {@code node} to the value of the {@code transferResult}. Returns
+ * true if the node's value changed, or a store was updated.
*/
protected boolean updateNodeValues(Node node, TransferResult<A, S> transferResult) {
- A newVal = transferResult.getResultValue();
- boolean nodeValueChanged = false;
+ A newVal = transferResult.getResultValue();
+ boolean nodeValueChanged = false;
- if (newVal != null) {
- A oldVal = nodeValues.get(node);
- nodeValues.put(node, newVal);
- nodeValueChanged = !Objects.equals(oldVal, newVal);
- }
+ if (newVal != null) {
+ A oldVal = nodeValues.get(node);
+ nodeValues.put(node, newVal);
+ nodeValueChanged = !Objects.equals(oldVal, newVal);
+ }
- return nodeValueChanged || transferResult.storeChanged();
+ return nodeValueChanged || transferResult.storeChanged();
}
/**
- * Call the transfer function for node {@code node}, and set that node as
- * current node first.
+ * Call the transfer function for node {@code node}, and set that node as current node first.
*/
- protected TransferResult<A, S> callTransferFunction(Node node,
- TransferInput<A, S> store) {
+ protected TransferResult<A, S> callTransferFunction(Node node, TransferInput<A, S> store) {
if (node.isLValue()) {
// TODO: should the default behavior be to return either a regular
// transfer result or a conditional transfer result (depending on
// store.hasTwoStores()), or is the following correct?
- return new RegularTransferResult<A, S>(null,
- store.getRegularStore());
+ return new RegularTransferResult<A, S>(null, store.getRegularStore());
}
store.node = node;
currentNode = node;
- TransferResult<A, S> transferResult = node.accept(transferFunction,
- store);
+ TransferResult<A, S> transferResult = node.accept(transferFunction, store);
currentNode = null;
if (node instanceof ReturnNode) {
// save a copy of the store to later check if some property held at
@@ -389,6 +428,7 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
this.cfg = cfg;
thenStores = new IdentityHashMap<>();
elseStores = new IdentityHashMap<>();
+ blockCount = maxCountBeforeWidening == -1 ? null : new IdentityHashMap<Block, Integer>();
inputs = new IdentityHashMap<>();
storesAtReturnStatements = new IdentityHashMap<>();
worklist = new Worklist(cfg);
@@ -428,8 +468,7 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
/**
- * Add a basic block to the worklist. If <code>b</code> is already present,
- * the method does nothing.
+ * Add a basic block to the worklist. If {@code b} is already present, the method does nothing.
*/
protected void addToWorklist(Block b) {
// TODO: use a more efficient way to check if b is already present
@@ -439,74 +478,84 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
/**
- * Add a store before the basic block <code>b</code> by merging with the
- * existing stores for that location.
+ * Add a store before the basic block {@code b} by merging with the existing stores for that
+ * location.
*/
- protected void addStoreBefore(Block b, Node node, S s, Store.Kind kind,
- boolean addBlockToWorklist) {
+ protected void addStoreBefore(
+ Block b, Node node, S s, Store.Kind kind, boolean addBlockToWorklist) {
S thenStore = getStoreBefore(b, Store.Kind.THEN);
S elseStore = getStoreBefore(b, Store.Kind.ELSE);
-
- switch (kind) {
- case THEN: {
- // Update the then store
- S newThenStore = (thenStore != null) ?
- thenStore.leastUpperBound(s) : s;
- if (!newThenStore.equals(thenStore)) {
- thenStores.put(b, newThenStore);
- if (elseStore != null) {
- inputs.put(b, new TransferInput<>(node, this, newThenStore, elseStore));
- addBlockToWorklist = true;
- }
+ boolean shouldWiden = false;
+ if (blockCount != null) {
+ Integer count = blockCount.get(b);
+ if (count == null) {
+ count = 0;
}
- break;
- }
- case ELSE: {
- // Update the else store
- S newElseStore = (elseStore != null) ?
- elseStore.leastUpperBound(s) : s;
- if (!newElseStore.equals(elseStore)) {
- elseStores.put(b, newElseStore);
- if (thenStore != null) {
- inputs.put(b, new TransferInput<>(node, this, thenStore, newElseStore));
- addBlockToWorklist = true;
- }
+ shouldWiden = count >= maxCountBeforeWidening;
+ if (shouldWiden) {
+ blockCount.put(b, 0);
+ } else {
+ blockCount.put(b, count + 1);
}
- break;
}
- case BOTH:
- if (thenStore == elseStore) {
- // Currently there is only one regular store
- S newStore = (thenStore != null) ?
- thenStore.leastUpperBound(s) : s;
- if (!newStore.equals(thenStore)) {
- thenStores.put(b, newStore);
- elseStores.put(b, newStore);
- inputs.put(b, new TransferInput<>(node, this, newStore));
- addBlockToWorklist = true;
- }
- } else {
- boolean storeChanged = false;
- S newThenStore = (thenStore != null) ?
- thenStore.leastUpperBound(s) : s;
- if (!newThenStore.equals(thenStore)) {
- thenStores.put(b, newThenStore);
- storeChanged = true;
+ switch (kind) {
+ case THEN:
+ {
+ // Update the then store
+ S newThenStore = mergeStores(s, thenStore, shouldWiden);
+ if (!newThenStore.equals(thenStore)) {
+ thenStores.put(b, newThenStore);
+ if (elseStore != null) {
+ inputs.put(b, new TransferInput<>(node, this, newThenStore, elseStore));
+ addBlockToWorklist = true;
+ }
+ }
+ break;
}
-
- S newElseStore = (elseStore != null) ?
- elseStore.leastUpperBound(s) : s;
- if (!newElseStore.equals(elseStore)) {
- elseStores.put(b, newElseStore);
- storeChanged = true;
+ case ELSE:
+ {
+ // Update the else store
+ S newElseStore = mergeStores(s, elseStore, shouldWiden);
+ if (!newElseStore.equals(elseStore)) {
+ elseStores.put(b, newElseStore);
+ if (thenStore != null) {
+ inputs.put(b, new TransferInput<>(node, this, thenStore, newElseStore));
+ addBlockToWorklist = true;
+ }
+ }
+ break;
}
+ case BOTH:
+ if (thenStore == elseStore) {
+ // Currently there is only one regular store
+ S newStore = mergeStores(s, thenStore, shouldWiden);
+ if (!newStore.equals(thenStore)) {
+ thenStores.put(b, newStore);
+ elseStores.put(b, newStore);
+ inputs.put(b, new TransferInput<>(node, this, newStore));
+ addBlockToWorklist = true;
+ }
+ } else {
+ boolean storeChanged = false;
+
+ S newThenStore = mergeStores(s, thenStore, shouldWiden);
+ if (!newThenStore.equals(thenStore)) {
+ thenStores.put(b, newThenStore);
+ storeChanged = true;
+ }
+
+ S newElseStore = mergeStores(s, elseStore, shouldWiden);
+ if (!newElseStore.equals(elseStore)) {
+ elseStores.put(b, newElseStore);
+ storeChanged = true;
+ }
- if (storeChanged) {
- inputs.put(b, new TransferInput<>(node, this, newThenStore, newElseStore));
- addBlockToWorklist = true;
+ if (storeChanged) {
+ inputs.put(b, new TransferInput<>(node, this, newThenStore, newElseStore));
+ addBlockToWorklist = true;
+ }
}
- }
}
if (addBlockToWorklist) {
@@ -514,17 +563,26 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
}
+ private S mergeStores(S newStore, S previousStore, boolean shouldWiden) {
+ if (previousStore == null) {
+ return newStore;
+ } else if (shouldWiden) {
+ return newStore.widenedUpperBound(previousStore);
+ } else {
+ return newStore.leastUpperBound(previousStore);
+ }
+ }
+
/**
- * A worklist is a priority queue of blocks in which the order is given
- * by depth-first ordering to place non-loop predecessors ahead of successors.
+ * A worklist is a priority queue of blocks in which the order is given by depth-first ordering
+ * to place non-loop predecessors ahead of successors.
*/
protected static class Worklist {
/** Map all blocks in the CFG to their depth-first order. */
protected IdentityHashMap<Block, Integer> depthFirstOrder;
- /** Comparator to allow priority queue to order blocks by their depth-first
- order. */
+ /** Comparator to allow priority queue to order blocks by their depth-first order. */
public class DFOComparator implements Comparator<Block> {
@Override
public int compare(Block b1, Block b2) {
@@ -535,7 +593,6 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
/** The backing priority queue. */
protected PriorityQueue<Block> queue;
-
public Worklist(ControlFlowGraph cfg) {
depthFirstOrder = new IdentityHashMap<>();
int count = 1;
@@ -569,43 +626,39 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
/**
- * Read the {@link TransferInput} for a particular basic block (or {@code null} if
- * none exists yet).
+ * Read the {@link TransferInput} for a particular basic block (or {@code null} if none exists
+ * yet).
*/
public /*@Nullable*/ TransferInput<A, S> getInput(Block b) {
return getInputBefore(b);
}
/**
- * @return The transfer input corresponding to the location right before the basic
- * block <code>b</code>.
+ * @return the transfer input corresponding to the location right before the basic block {@code
+ * b}.
*/
protected /*@Nullable*/ TransferInput<A, S> getInputBefore(Block b) {
return inputs.get(b);
}
- /**
- * @return The store corresponding to the location right before the basic
- * block <code>b</code>.
- */
+ /** @return the store corresponding to the location right before the basic block {@code b}. */
protected /*@Nullable*/ S getStoreBefore(Block b, Store.Kind kind) {
switch (kind) {
- case THEN:
- return readFromStore(thenStores, b);
- case ELSE:
- return readFromStore(elseStores, b);
- default:
- assert false;
- return null;
+ case THEN:
+ return readFromStore(thenStores, b);
+ case ELSE:
+ return readFromStore(elseStores, b);
+ default:
+ assert false;
+ return null;
}
}
/**
- * Read the {@link Store} for a particular basic block from a map of stores
- * (or {@code null} if none exists yet).
+ * Read the {@link Store} for a particular basic block from a map of stores (or {@code null} if
+ * none exists yet).
*/
- protected static <S> /*@Nullable*/ S readFromStore(Map<Block, S> stores,
- Block b) {
+ protected static <S> /*@Nullable*/ S readFromStore(Map<Block, S> stores, Block b) {
return stores.get(b);
}
@@ -615,24 +668,24 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
/**
- * @return The abstract value for {@link Node} {@code n}, or {@code null} if
- * no information is available. Note that if the analysis has not
- * finished yet, this value might not represent the final value for
- * this node.
+ * @return the abstract value for {@link Node} {@code n}, or {@code null} if no information is
+ * available. Note that if the analysis has not finished yet, this value might not represent
+ * the final value for this node.
*/
public /*@Nullable*/ A getValue(Node n) {
if (isRunning) {
// we do not yet have a org.checkerframework.dataflow fact about the current node
- if (currentNode == n
+ if (currentNode == null
+ || currentNode == n
|| (currentTree != null && currentTree == n.getTree())) {
return null;
}
// check that 'n' is a subnode of 'node'. Check immediate operands
// first for efficiency.
- assert currentNode != null;
assert !n.isLValue() : "Did not expect an lvalue, but got " + n;
- if (!(currentNode != n && (currentNode.getOperands().contains(n) || currentNode
- .getTransitiveOperands().contains(n)))) {
+ if (!(currentNode != n
+ && (currentNode.getOperands().contains(n)
+ || currentNode.getTransitiveOperands().contains(n)))) {
return null;
}
return nodeValues.get(n);
@@ -641,10 +694,9 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
/**
- * @return The abstract value for {@link Tree} {@code t}, or {@code null} if
- * no information is available. Note that if the analysis has not
- * finished yet, this value might not represent the final value for
- * this node.
+ * @return the abstract value for {@link Tree} {@code t}, or {@code null} if no information is
+ * available. Note that if the analysis has not finished yet, this value might not represent
+ * the final value for this node.
*/
public /*@Nullable*/ A getValue(Tree t) {
// we do not yet have a org.checkerframework.dataflow fact about the current node
@@ -658,24 +710,22 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
return getValue(nodeCorrespondingToTree);
}
- /**
- * Get the {@link Node} for a given {@link Tree}.
- */
+ /** Get the {@link Node} for a given {@link Tree}. */
public Node getNodeForTree(Tree t) {
return cfg.getNodeCorrespondingToTree(t);
}
/**
- * Get the {@link MethodTree} of the current CFG if the argument {@link Tree} maps
- * to a {@link Node} in the CFG or null otherwise.
+ * Get the {@link MethodTree} of the current CFG if the argument {@link Tree} maps to a {@link
+ * Node} in the CFG or null otherwise.
*/
public /*@Nullable*/ MethodTree getContainingMethod(Tree t) {
return cfg.getContainingMethod(t);
}
/**
- * Get the {@link ClassTree} of the current CFG if the argument {@link Tree} maps
- * to a {@link Node} in the CFG or null otherwise.
+ * Get the {@link ClassTree} of the current CFG if the argument {@link Tree} maps to a {@link
+ * Node} in the CFG or null otherwise.
*/
public /*@Nullable*/ ClassTree getContainingClass(Tree t) {
return cfg.getContainingClass(t);
@@ -684,8 +734,7 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
public List<Pair<ReturnNode, TransferResult<A, S>>> getReturnStatementStores() {
List<Pair<ReturnNode, TransferResult<A, S>>> result = new ArrayList<>();
for (ReturnNode returnNode : cfg.getReturnNodes()) {
- TransferResult<A, S> store = storesAtReturnStatements
- .get(returnNode);
+ TransferResult<A, S> store = storesAtReturnStatements.get(returnNode);
result.add(Pair.of(returnNode, store));
}
return result;
@@ -698,9 +747,8 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
/**
- * @return The regular exit store, or {@code null}, if there is no such
- * store (because the method cannot exit through the regular exit
- * block).
+ * @return the regular exit store, or {@code null}, if there is no such store (because the
+ * method cannot exit through the regular exit block).
*/
public /*@Nullable*/ S getRegularExitStore() {
SpecialBlock regularExitBlock = cfg.getRegularExitBlock();
@@ -713,8 +761,7 @@ public class Analysis<A extends AbstractValue<A>, S extends Store<S>, T extends
}
public S getExceptionalExitStore() {
- S exceptionalExitStore = inputs.get(cfg.getExceptionalExitBlock())
- .getRegularStore();
+ S exceptionalExitStore = inputs.get(cfg.getExceptionalExitBlock()).getRegularStore();
return exceptionalExitStore;
}
}