diff options
Diffstat (limited to 'third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis')
10 files changed, 1130 insertions, 831 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AbstractValue.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AbstractValue.java index 2dbcbd4b03..25b78075da 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AbstractValue.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AbstractValue.java @@ -4,23 +4,21 @@ package org.checkerframework.dataflow.analysis; * An abstract value used in the org.checkerframework.dataflow analysis. * * @author Stefan Heule - * */ public interface AbstractValue<V extends AbstractValue<V>> { /** * Compute the least upper bound of two stores. * - * <p> + * <p><em>Important</em>: This method must fulfill the following contract: * - * <em>Important</em>: This method must fulfill the following contract: * <ul> - * <li>Does not change {@code this}.</li> - * <li>Does not change {@code other}.</li> - * <li>Returns a fresh object which is not aliased yet.</li> - * <li>Returns an object of the same (dynamic) type as {@code this}, even if - * the signature is more permissive.</li> - * <li>Is commutative.</li> + * <li>Does not change {@code this}. + * <li>Does not change {@code other}. + * <li>Returns a fresh object which is not aliased yet. + * <li>Returns an object of the same (dynamic) type as {@code this}, even if the signature is + * more permissive. + * <li>Is commutative. * </ul> */ V leastUpperBound(V other); 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 ==> (currentNode == null) + * !isRunning ⇒ (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; } } diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AnalysisResult.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AnalysisResult.java index 42b8d2f2ba..48f376dbea 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AnalysisResult.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/AnalysisResult.java @@ -4,29 +4,24 @@ package org.checkerframework.dataflow.analysis; import org.checkerframework.checker.nullness.qual.Nullable; */ -import org.checkerframework.dataflow.cfg.block.Block; -import org.checkerframework.dataflow.cfg.block.ExceptionBlock; -import org.checkerframework.dataflow.cfg.block.RegularBlock; -import org.checkerframework.dataflow.cfg.node.Node; - +import com.sun.source.tree.Tree; import java.util.HashMap; import java.util.IdentityHashMap; import java.util.Map; import java.util.Map.Entry; - import javax.lang.model.element.Element; - -import com.sun.source.tree.Tree; +import org.checkerframework.dataflow.cfg.block.Block; +import org.checkerframework.dataflow.cfg.block.ExceptionBlock; +import org.checkerframework.dataflow.cfg.block.RegularBlock; +import org.checkerframework.dataflow.cfg.node.Node; /** * An {@link AnalysisResult} represents the result of a org.checkerframework.dataflow analysis by - * providing the abstract values given a node or a tree. Note that it does not - * keep track of custom results computed by some analysis. + * providing the abstract values given a node or a tree. Note that it does not keep track of custom + * results computed by some analysis. * * @author Stefan Heule - * - * @param <A> - * type of the abstract value that is tracked. + * @param <A> type of the abstract value that is tracked */ public class AnalysisResult<A extends AbstractValue<A>, S extends Store<S>> { @@ -39,26 +34,22 @@ public class AnalysisResult<A extends AbstractValue<A>, S extends Store<S>> { /** Map from (effectively final) local variable elements to their abstract value. */ protected final HashMap<Element, A> finalLocalValues; - /** - * The stores before every method call. - */ + /** The stores before every method call. */ protected final IdentityHashMap<Block, TransferInput<A, S>> stores; - /** - * Initialize with a given node-value mapping. - */ - public AnalysisResult(Map<Node, A> nodeValues, + /** Initialize with a given node-value mapping. */ + public AnalysisResult( + Map<Node, A> nodeValues, IdentityHashMap<Block, TransferInput<A, S>> stores, - IdentityHashMap<Tree, Node> treeLookup, HashMap<Element, A> finalLocalValues) { + IdentityHashMap<Tree, Node> treeLookup, + HashMap<Element, A> finalLocalValues) { this.nodeValues = new IdentityHashMap<>(nodeValues); this.treeLookup = new IdentityHashMap<>(treeLookup); this.stores = stores; this.finalLocalValues = finalLocalValues; } - /** - * Initialize empty result. - */ + /** Initialize empty result. */ public AnalysisResult() { nodeValues = new IdentityHashMap<>(); treeLookup = new IdentityHashMap<>(); @@ -66,9 +57,7 @@ public class AnalysisResult<A extends AbstractValue<A>, S extends Store<S>> { finalLocalValues = new HashMap<>(); } - /** - * Combine with another analysis result. - */ + /** Combine with another analysis result. */ public void combine(AnalysisResult<A, S> other) { for (Entry<Node, A> e : other.nodeValues.entrySet()) { nodeValues.put(e.getKey(), e.getValue()); @@ -84,68 +73,68 @@ public class AnalysisResult<A extends AbstractValue<A>, S extends Store<S>> { } } - /** - * @return The value of effectively final local variables. - */ + /** @return the value of effectively final local variables */ public HashMap<Element, A> getFinalLocalValues() { return finalLocalValues; } /** - * @return The abstract value for {@link Node} {@code n}, or {@code null} if - * no information is available. + * @return the abstract value for {@link Node} {@code n}, or {@code null} if no information is + * available. */ public /*@Nullable*/ A getValue(Node n) { return nodeValues.get(n); } /** - * @return The abstract value for {@link Tree} {@code t}, or {@code null} if - * no information is available. + * @return the abstract value for {@link Tree} {@code t}, or {@code null} if no information is + * available. */ public /*@Nullable*/ A getValue(Tree t) { A val = getValue(treeLookup.get(t)); return val; } - /** - * @return The {@link Node} for a given {@link Tree}. - */ + /** @return the {@link Node} for a given {@link Tree}. */ public /*@Nullable*/ Node getNodeForTree(Tree tree) { return treeLookup.get(tree); } - /** - * @return The store immediately before a given {@link Tree}. - */ + /** @return the store immediately before a given {@link Tree}. */ public S getStoreBefore(Tree tree) { Node node = getNodeForTree(tree); if (node == null) { return null; } + return getStoreBefore(node); + } + + /** @return the store immediately before a given {@link Node}. */ + public S getStoreBefore(Node node) { return runAnalysisFor(node, true); } - /** - * @return The store immediately after a given {@link Tree}. - */ + /** @return the store immediately after a given {@link Tree}. */ public S getStoreAfter(Tree tree) { Node node = getNodeForTree(tree); if (node == null) { return null; } + return getStoreAfter(node); + } + + /** @return the store immediately after a given {@link Node}. */ + public S getStoreAfter(Node node) { return runAnalysisFor(node, false); } /** - * Runs the analysis again within the block of {@code node} and returns the - * store at the location of {@code node}. If {@code before} is true, then - * the store immediately before the {@link Node} {@code node} is returned. - * Otherwise, the store after {@code node} is returned. + * Runs the analysis again within the block of {@code node} and returns the store at the + * location of {@code node}. If {@code before} is true, then the store immediately before the + * {@link Node} {@code node} is returned. Otherwise, the store after {@code node} is returned. * - * <p> - * If the given {@link Node} cannot be reached (in the control flow graph), - * then {@code null} is returned. + * <p>If the given {@link Node} cannot be reached (in the control flow graph), then {@code null} + * is returned. */ protected S runAnalysisFor(Node node, boolean before) { Block block = node.getBlock(); @@ -157,10 +146,9 @@ public class AnalysisResult<A extends AbstractValue<A>, S extends Store<S>> { } /** - * Runs the analysis again within the block of {@code node} and returns the - * store at the location of {@code node}. If {@code before} is true, then - * the store immediately before the {@link Node} {@code node} is returned. - * Otherwise, the store after {@code node} is returned. + * Runs the analysis again within the block of {@code node} and returns the store at the + * location of {@code node}. If {@code before} is true, then the store immediately before the + * {@link Node} {@code node} is returned. Otherwise, the store after {@code node} is returned. */ public static <A extends AbstractValue<A>, S extends Store<S>> S runAnalysisFor( Node node, boolean before, TransferInput<A, S> transferInput) { @@ -176,49 +164,51 @@ public class AnalysisResult<A extends AbstractValue<A>, S extends Store<S>> { analysis.isRunning = true; try { switch (block.getType()) { - case REGULAR_BLOCK: { - RegularBlock rb = (RegularBlock) block; - - // Apply transfer function to contents until we found the node - // we - // are looking for. - TransferInput<A, S> store = transferInput; - TransferResult<A, S> transferResult = null; - for (Node n : rb.getContents()) { - analysis.currentNode = n; - if (n == node && before) { - return store.getRegularStore(); + case REGULAR_BLOCK: + { + RegularBlock rb = (RegularBlock) block; + + // Apply transfer function to contents until we found the node + // we + // are looking for. + TransferInput<A, S> store = transferInput; + TransferResult<A, S> transferResult = null; + for (Node n : rb.getContents()) { + analysis.currentNode = n; + if (n == node && before) { + return store.getRegularStore(); + } + transferResult = analysis.callTransferFunction(n, store); + if (n == node) { + return transferResult.getRegularStore(); + } + store = new TransferInput<>(n, analysis, transferResult); + } + // This point should never be reached. If the block of 'node' is + // 'block', then 'node' must be part of the contents of 'block'. + assert false; + return null; } - transferResult = analysis.callTransferFunction(n, store); - if (n == node) { + + case EXCEPTION_BLOCK: + { + ExceptionBlock eb = (ExceptionBlock) block; + + // apply transfer function to content + assert eb.getNode() == node; + if (before) { + return transferInput.getRegularStore(); + } + analysis.currentNode = node; + TransferResult<A, S> transferResult = + analysis.callTransferFunction(node, transferInput); return transferResult.getRegularStore(); } - store = new TransferInput<>(n, analysis, transferResult); - } - // This point should never be reached. If the block of 'node' is - // 'block', then 'node' must be part of the contents of 'block'. - assert false; - return null; - } - - case EXCEPTION_BLOCK: { - ExceptionBlock eb = (ExceptionBlock) block; - - // apply transfer function to content - assert eb.getNode() == node; - if (before) { - return transferInput.getRegularStore(); - } - analysis.currentNode = node; - TransferResult<A, S> transferResult = analysis - .callTransferFunction(node, transferInput); - return transferResult.getRegularStore(); - } - default: - // Only regular blocks and exceptional blocks can hold nodes. - assert false; - break; + default: + // Only regular blocks and exceptional blocks can hold nodes. + assert false; + break; } return null; diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/ConditionalTransferResult.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/ConditionalTransferResult.java index c49357a3ff..99a8a525ec 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/ConditionalTransferResult.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/ConditionalTransferResult.java @@ -1,19 +1,15 @@ package org.checkerframework.dataflow.analysis; import java.util.Map; - import javax.lang.model.type.TypeMirror; /** - * Implementation of a {@link TransferResult} with two non-exceptional store; - * one for the 'then' edge and one for 'else'. The result of - * {@code getRegularStore} will be the least upper bound of the two underlying - * stores. + * Implementation of a {@link TransferResult} with two non-exceptional store; one for the 'then' + * edge and one for 'else'. The result of {@code getRegularStore} will be the least upper bound of + * the two underlying stores. * * @author Stefan Heule - * - * @param <S> - * The {@link Store} used to keep track of intermediate results. + * @param <S> the {@link Store} used to keep track of intermediate results */ public class ConditionalTransferResult<A extends AbstractValue<A>, S extends Store<S>> extends TransferResult<A, S> { @@ -27,25 +23,21 @@ public class ConditionalTransferResult<A extends AbstractValue<A>, S extends Sto protected S elseStore; /** - * Create a {@code ConditionalTransferResult} with {@code thenStore} as the - * resulting store if the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} evaluates to - * {@code true} and {@code elseStore} otherwise. - * - * For the meaning of storeChanged, see - * {@link org.checkerframework.dataflow.analysis.TransferResult#storeChanged}. + * Create a {@code ConditionalTransferResult} with {@code thenStore} as the resulting store if + * the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} evaluates to {@code + * true} and {@code elseStore} otherwise. * - * <p> + * <p>For the meaning of storeChanged, see {@link + * org.checkerframework.dataflow.analysis.TransferResult#storeChanged}. * - * <em>Exceptions</em>: If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} throws an - * exception, then it is assumed that no special handling is necessary and - * the store before the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} will be passed along any - * exceptional edge. + * <p><em>Exceptions</em>: If the corresponding {@link + * org.checkerframework.dataflow.cfg.node.Node} throws an exception, then it is assumed that no + * special handling is necessary and the store before the corresponding {@link + * org.checkerframework.dataflow.cfg.node.Node} will be passed along any exceptional edge. * - * <p> - * - * <em>Aliasing</em>: {@code thenStore} and {@code elseStore} are not - * allowed to be used anywhere outside of this class (including use through - * aliases). Complete control over the objects is transfered to this class. + * <p><em>Aliasing</em>: {@code thenStore} and {@code elseStore} are not allowed to be used + * anywhere outside of this class (including use through aliases). Complete control over the + * objects is transfered to this class. */ public ConditionalTransferResult(A value, S thenStore, S elseStore, boolean storeChanged) { super(value); @@ -59,27 +51,27 @@ public class ConditionalTransferResult<A extends AbstractValue<A>, S extends Sto } /** - * Create a {@code ConditionalTransferResult} with {@code thenStore} as the - * resulting store if the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} evaluates to - * {@code true} and {@code elseStore} otherwise. - * - * <p> + * Create a {@code ConditionalTransferResult} with {@code thenStore} as the resulting store if + * the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} evaluates to {@code + * true} and {@code elseStore} otherwise. * - * <em>Exceptions</em>: If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} throws an - * exception, then the corresponding store in {@code exceptionalStores} is - * used. If no exception is found in {@code exceptionalStores}, then it is - * assumed that no special handling is necessary and the store before the - * corresponding {@link org.checkerframework.dataflow.cfg.node.Node} will be passed along any exceptional edge. + * <p><em>Exceptions</em>: If the corresponding {@link + * org.checkerframework.dataflow.cfg.node.Node} throws an exception, then the corresponding + * store in {@code exceptionalStores} is used. If no exception is found in {@code + * exceptionalStores}, then it is assumed that no special handling is necessary and the store + * before the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} will be passed + * along any exceptional edge. * - * <p> - * - * <em>Aliasing</em>: {@code thenStore}, {@code elseStore}, and any store in - * {@code exceptionalStores} are not allowed to be used anywhere outside of - * this class (including use through aliases). Complete control over the - * objects is transfered to this class. + * <p><em>Aliasing</em>: {@code thenStore}, {@code elseStore}, and any store in {@code + * exceptionalStores} are not allowed to be used anywhere outside of this class (including use + * through aliases). Complete control over the objects is transfered to this class. */ - public ConditionalTransferResult(A value, S thenStore, S elseStore, - Map<TypeMirror, S> exceptionalStores, boolean storeChanged) { + public ConditionalTransferResult( + A value, + S thenStore, + S elseStore, + Map<TypeMirror, S> exceptionalStores, + boolean storeChanged) { super(value); this.exceptionalStores = exceptionalStores; this.thenStore = thenStore; @@ -87,8 +79,8 @@ public class ConditionalTransferResult<A extends AbstractValue<A>, S extends Sto this.storeChanged = storeChanged; } - public ConditionalTransferResult(A value, S thenStore, S elseStore, - Map<TypeMirror, S> exceptionalStores) { + public ConditionalTransferResult( + A value, S thenStore, S elseStore, Map<TypeMirror, S> exceptionalStores) { this(value, thenStore, elseStore, exceptionalStores, false); } @@ -126,12 +118,9 @@ public class ConditionalTransferResult<A extends AbstractValue<A>, S extends Sto return result.toString(); } - /** - * @see org.checkerframework.dataflow.analysis.TransferResult#storeChanged() - */ + /** @see org.checkerframework.dataflow.analysis.TransferResult#storeChanged() */ @Override public boolean storeChanged() { - return storeChanged; + return storeChanged; } - } diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/FlowExpressions.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/FlowExpressions.java index 54828c7d31..85ad7b4b00 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/FlowExpressions.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/FlowExpressions.java @@ -1,6 +1,25 @@ package org.checkerframework.dataflow.analysis; +import com.sun.source.tree.ArrayAccessTree; +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.LiteralTree; +import com.sun.source.tree.MemberSelectTree; +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.VariableTree; +import com.sun.source.util.TreePath; +import com.sun.tools.javac.code.Symbol.VarSymbol; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; +import org.checkerframework.dataflow.cfg.node.ArrayCreationNode; import org.checkerframework.dataflow.cfg.node.ClassNameNode; import org.checkerframework.dataflow.cfg.node.ExplicitThisLiteralNode; import org.checkerframework.dataflow.cfg.node.FieldAccessNode; @@ -15,41 +34,33 @@ import org.checkerframework.dataflow.cfg.node.ValueLiteralNode; import org.checkerframework.dataflow.cfg.node.WideningConversionNode; import org.checkerframework.dataflow.util.HashCodeUtils; import org.checkerframework.dataflow.util.PurityUtils; - import org.checkerframework.javacutil.AnnotationProvider; import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.ErrorReporter; +import org.checkerframework.javacutil.InternalUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypeAnnotationUtils; import org.checkerframework.javacutil.TypesUtils; -import java.util.ArrayList; -import java.util.List; - -import javax.lang.model.element.Element; -import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.VariableElement; -import javax.lang.model.type.TypeKind; -import javax.lang.model.type.TypeMirror; - /** - * Collection of classes and helper functions to represent Java expressions - * about which the org.checkerframework.dataflow analysis can possibly infer facts. Expressions - * include: + * Collection of classes and helper functions to represent Java expressions about which the + * org.checkerframework.dataflow analysis can possibly infer facts. Expressions include: + * * <ul> - * <li>Field accesses (e.g., <em>o.f</em>)</li> - * <li>Local variables (e.g., <em>l</em>)</li> - * <li>This reference (e.g., <em>this</em>)</li> - * <li>Pure method calls (e.g., <em>o.m()</em>)</li> - * <li>Unknown other expressions to mark that something else was present.</li> + * <li>Field accesses (e.g., <em>o.f</em>) + * <li>Local variables (e.g., <em>l</em>) + * <li>This reference (e.g., <em>this</em>) + * <li>Pure method calls (e.g., <em>o.m()</em>) + * <li>Unknown other expressions to mark that something else was present. * </ul> * * @author Stefan Heule - * */ public class FlowExpressions { /** - * @return The internal representation (as {@link FieldAccess}) of a - * {@link FieldAccessNode}. Can contain {@link Unknown} as receiver. + * @return the internal representation (as {@link FieldAccess}) of a {@link FieldAccessNode}. + * Can contain {@link Unknown} as receiver. */ public static FieldAccess internalReprOfFieldAccess( AnnotationProvider provider, FieldAccessNode node) { @@ -64,8 +75,8 @@ public class FlowExpressions { } /** - * @return The internal representation (as {@link FieldAccess}) of a - * {@link FieldAccessNode}. Can contain {@link Unknown} as receiver. + * @return the internal representation (as {@link FieldAccess}) of a {@link FieldAccessNode}. + * Can contain {@link Unknown} as receiver. */ public static ArrayAccess internalReprOfArrayAccess( AnnotationProvider provider, ArrayAccessNode node) { @@ -75,26 +86,25 @@ public class FlowExpressions { } /** - * We ignore operations such as widening and - * narrowing when computing the internal representation. + * We ignore operations such as widening and narrowing when computing the internal + * representation. * - * @return The internal representation (as {@link Receiver}) of any - * {@link Node}. Might contain {@link Unknown}. + * @return the internal representation (as {@link Receiver}) of any {@link Node}. Might contain + * {@link Unknown}. */ - public static Receiver internalReprOf(AnnotationProvider provider, - Node receiverNode) { + public static Receiver internalReprOf(AnnotationProvider provider, Node receiverNode) { return internalReprOf(provider, receiverNode, false); } /** - * We ignore operations such as widening and - * narrowing when computing the internal representation. + * We ignore operations such as widening and narrowing when computing the internal + * representation. * - * @return The internal representation (as {@link Receiver}) of any - * {@link Node}. Might contain {@link Unknown}. + * @return the internal representation (as {@link Receiver}) of any {@link Node}. Might contain + * {@link Unknown}. */ - public static Receiver internalReprOf(AnnotationProvider provider, - Node receiverNode, boolean allowNonDeterminitic) { + public static Receiver internalReprOf( + AnnotationProvider provider, Node receiverNode, boolean allowNonDeterministic) { Receiver receiver = null; if (receiverNode instanceof FieldAccessNode) { FieldAccessNode fan = (FieldAccessNode) receiverNode; @@ -103,6 +113,12 @@ public class FlowExpressions { // For some reason, "className.this" is considered a field access. // We right this wrong here. receiver = new ThisReference(fan.getReceiver().getType()); + } else if (fan.getFieldName().equals("class")) { + // "className.class" is considered a field access. This makes sense, + // since .class is similar to a field access which is the equivalent + // of a call to getClass(). However for the purposes of dataflow + // analysis, and value stores, this is the equivalent of a ClassNameNode. + receiver = new ClassName(fan.getReceiver().getType()); } else { receiver = internalReprOfFieldAccess(provider, fan); } @@ -120,26 +136,25 @@ public class FlowExpressions { receiver = internalReprOfArrayAccess(provider, a); } else if (receiverNode instanceof StringConversionNode) { // ignore string conversion - return internalReprOf(provider, - ((StringConversionNode) receiverNode).getOperand()); + return internalReprOf(provider, ((StringConversionNode) receiverNode).getOperand()); } else if (receiverNode instanceof WideningConversionNode) { // ignore widening - return internalReprOf(provider, - ((WideningConversionNode) receiverNode).getOperand()); + return internalReprOf(provider, ((WideningConversionNode) receiverNode).getOperand()); } else if (receiverNode instanceof NarrowingConversionNode) { // ignore narrowing - return internalReprOf(provider, - ((NarrowingConversionNode) receiverNode).getOperand()); + return internalReprOf(provider, ((NarrowingConversionNode) receiverNode).getOperand()); } else if (receiverNode instanceof ClassNameNode) { ClassNameNode cn = (ClassNameNode) receiverNode; receiver = new ClassName(cn.getType()); } else if (receiverNode instanceof ValueLiteralNode) { ValueLiteralNode vn = (ValueLiteralNode) receiverNode; receiver = new ValueLiteral(vn.getType(), vn); + } else if (receiverNode instanceof ArrayCreationNode) { + ArrayCreationNode an = (ArrayCreationNode) receiverNode; + receiver = new ArrayCreation(an.getType(), an.getDimensions(), an.getInitializers()); } else if (receiverNode instanceof MethodInvocationNode) { MethodInvocationNode mn = (MethodInvocationNode) receiverNode; - ExecutableElement invokedMethod = TreeUtils.elementFromUse(mn - .getTree()); + ExecutableElement invokedMethod = TreeUtils.elementFromUse(mn.getTree()); // check if this represents a boxing operation of a constant, in which // case we treat the method call as deterministic, because there is no way @@ -153,21 +168,20 @@ public class FlowExpressions { } } - if (PurityUtils.isDeterministic(provider, invokedMethod) || allowNonDeterminitic || considerDeterministic) { + if (PurityUtils.isDeterministic(provider, invokedMethod) + || allowNonDeterministic + || considerDeterministic) { List<Receiver> parameters = new ArrayList<>(); for (Node p : mn.getArguments()) { parameters.add(internalReprOf(provider, p)); } Receiver methodReceiver; if (ElementUtils.isStatic(invokedMethod)) { - methodReceiver = new ClassName(mn.getTarget().getReceiver() - .getType()); + methodReceiver = new ClassName(mn.getTarget().getReceiver().getType()); } else { - methodReceiver = internalReprOf(provider, mn.getTarget() - .getReceiver()); + methodReceiver = internalReprOf(provider, mn.getTarget().getReceiver()); } - receiver = new PureMethodCall(mn.getType(), invokedMethod, - methodReceiver, parameters); + receiver = new MethodCall(mn.getType(), invokedMethod, methodReceiver, parameters); } } @@ -177,7 +191,209 @@ public class FlowExpressions { return receiver; } - public static abstract class Receiver { + /** + * @return the internal representation (as {@link Receiver}) of any {@link ExpressionTree}. + * Might contain {@link Unknown}. + */ + public static Receiver internalReprOf( + AnnotationProvider provider, ExpressionTree receiverTree) { + return internalReprOf(provider, receiverTree, true); + } + /** + * We ignore operations such as widening and narrowing when computing the internal + * representation. + * + * @return the internal representation (as {@link Receiver}) of any {@link ExpressionTree}. + * Might contain {@link Unknown}. + */ + public static Receiver internalReprOf( + AnnotationProvider provider, + ExpressionTree receiverTree, + boolean allowNonDeterministic) { + Receiver receiver; + switch (receiverTree.getKind()) { + case ARRAY_ACCESS: + ArrayAccessTree a = (ArrayAccessTree) receiverTree; + Receiver arrayAccessExpression = internalReprOf(provider, a.getExpression()); + Receiver index = internalReprOf(provider, a.getIndex()); + receiver = new ArrayAccess(InternalUtils.typeOf(a), arrayAccessExpression, index); + break; + case BOOLEAN_LITERAL: + case CHAR_LITERAL: + case DOUBLE_LITERAL: + case FLOAT_LITERAL: + case INT_LITERAL: + case LONG_LITERAL: + case NULL_LITERAL: + case STRING_LITERAL: + LiteralTree vn = (LiteralTree) receiverTree; + receiver = new ValueLiteral(InternalUtils.typeOf(receiverTree), vn.getValue()); + break; + case NEW_ARRAY: + receiver = + new ArrayCreation( + InternalUtils.typeOf(receiverTree), + Collections.<Node>emptyList(), + Collections.<Node>emptyList()); + break; + case METHOD_INVOCATION: + MethodInvocationTree mn = (MethodInvocationTree) receiverTree; + ExecutableElement invokedMethod = TreeUtils.elementFromUse(mn); + if (PurityUtils.isDeterministic(provider, invokedMethod) || allowNonDeterministic) { + List<Receiver> parameters = new ArrayList<>(); + for (ExpressionTree p : mn.getArguments()) { + parameters.add(internalReprOf(provider, p)); + } + Receiver methodReceiver; + if (ElementUtils.isStatic(invokedMethod)) { + methodReceiver = new ClassName(InternalUtils.typeOf(mn.getMethodSelect())); + } else { + methodReceiver = internalReprOf(provider, mn.getMethodSelect()); + } + TypeMirror type = InternalUtils.typeOf(mn); + receiver = new MethodCall(type, invokedMethod, methodReceiver, parameters); + } else { + receiver = null; + } + break; + case MEMBER_SELECT: + receiver = internalRepOfMemberSelect(provider, (MemberSelectTree) receiverTree); + break; + case IDENTIFIER: + IdentifierTree identifierTree = (IdentifierTree) receiverTree; + TypeMirror typeOfId = InternalUtils.typeOf(identifierTree); + if (identifierTree.getName().contentEquals("this") + || identifierTree.getName().contentEquals("super")) { + receiver = new ThisReference(typeOfId); + break; + } + Element ele = TreeUtils.elementFromUse(identifierTree); + switch (ele.getKind()) { + case LOCAL_VARIABLE: + case RESOURCE_VARIABLE: + case EXCEPTION_PARAMETER: + case PARAMETER: + receiver = new LocalVariable(ele); + break; + case FIELD: + // Implicit access expression, such as "this" or a class name + Receiver fieldAccessExpression; + TypeMirror enclosingType = ElementUtils.enclosingClass(ele).asType(); + if (ElementUtils.isStatic(ele)) { + fieldAccessExpression = new ClassName(enclosingType); + } else { + fieldAccessExpression = new ThisReference(enclosingType); + } + receiver = + new FieldAccess( + fieldAccessExpression, typeOfId, (VariableElement) ele); + break; + case CLASS: + case ENUM: + case ANNOTATION_TYPE: + case INTERFACE: + receiver = new ClassName(ele.asType()); + break; + default: + receiver = null; + } + break; + default: + receiver = null; + } + + if (receiver == null) { + receiver = new Unknown(InternalUtils.typeOf(receiverTree)); + } + return receiver; + } + + /** + * Returns the implicit receiver of ele. + * + * <p>Returns either a new ClassName or a new ThisReference depending on whether ele is static + * or not. The passed element must be a field, method, or class. + * + * @param ele field, method, or class + * @return either a new ClassName or a new ThisReference depending on whether ele is static or + * not + */ + public static Receiver internalRepOfImplicitReceiver(Element ele) { + TypeMirror enclosingType = ElementUtils.enclosingClass(ele).asType(); + if (ElementUtils.isStatic(ele)) { + return new ClassName(enclosingType); + } else { + return new ThisReference(enclosingType); + } + } + + /** + * Returns either a new ClassName or ThisReference Receiver object for the enclosingType + * + * <p>The Tree should be an expression or a statement that does not have a receiver or an + * implicit receiver. For example, a local variable declaration. + * + * @param path TreePath to tree + * @param enclosingType type of the enclosing type + * @return a new ClassName or ThisReference that is a Receiver object for the enclosingType + */ + public static Receiver internalRepOfPseudoReceiver(TreePath path, TypeMirror enclosingType) { + if (TreeUtils.isTreeInStaticScope(path)) { + return new ClassName(enclosingType); + } else { + return new ThisReference(enclosingType); + } + } + + private static Receiver internalRepOfMemberSelect( + AnnotationProvider provider, MemberSelectTree memberSelectTree) { + TypeMirror expressionType = InternalUtils.typeOf(memberSelectTree.getExpression()); + if (TreeUtils.isClassLiteral(memberSelectTree)) { + return new ClassName(expressionType); + } + Element ele = TreeUtils.elementFromUse(memberSelectTree); + switch (ele.getKind()) { + case METHOD: + case CONSTRUCTOR: + return internalReprOf(provider, memberSelectTree.getExpression()); + case CLASS: // o instanceof MyClass.InnerClass + case ENUM: + case INTERFACE: // o instanceof MyClass.InnerInterface + case ANNOTATION_TYPE: + return new ClassName(expressionType); + case ENUM_CONSTANT: + case FIELD: + Receiver r = internalReprOf(provider, memberSelectTree.getExpression()); + return new FieldAccess(r, ElementUtils.getType(ele), (VariableElement) ele); + default: + ErrorReporter.errorAbort( + "Unexpected element kind: %s element: %s", ele.getKind(), ele); + return null; + } + } + + /** + * Returns Receiver objects for the formal parameters of the method in which path is enclosed. + * + * @param annotationProvider annotationProvider + * @param path TreePath that is enclosed by the method + * @return list of Receiver objects for the formal parameters of the method in which path is + * enclosed + */ + public static List<Receiver> getParametersOfEnclosingMethod( + AnnotationProvider annotationProvider, TreePath path) { + MethodTree methodTree = TreeUtils.enclosingMethod(path); + if (methodTree == null) { + return null; + } + List<Receiver> internalArguments = new ArrayList<>(); + for (VariableTree arg : methodTree.getParameters()) { + internalArguments.add(internalReprOf(annotationProvider, new LocalVariableNode(arg))); + } + return internalArguments; + } + + public abstract static class Receiver { protected final TypeMirror type; public Receiver(TypeMirror type) { @@ -196,38 +412,32 @@ public class FlowExpressions { } /** - * Returns true if and only if the value this expression stands for - * cannot be changed by a method call. This is the case for local - * variables, the self reference as well as final field accesses for - * whose receiver {@link #isUnmodifiableByOtherCode} is true. + * Returns true if and only if the value this expression stands for cannot be changed by a + * method call. This is the case for local variables, the self reference as well as final + * field accesses for whose receiver {@link #isUnmodifiableByOtherCode} is true. */ public abstract boolean isUnmodifiableByOtherCode(); - /** - * @return True if and only if the two receiver are syntactically - * identical. - */ + /** @return true if and only if the two receiver are syntactically identical */ public boolean syntacticEquals(Receiver other) { return other == this; } /** - * @return True if and only if this receiver contains a receiver that is - * syntactically equal to {@code other}. + * @return true if and only if this receiver contains a receiver that is syntactically equal + * to {@code other}. */ public boolean containsSyntacticEqualReceiver(Receiver other) { return syntacticEquals(other); } /** - * Returns true if and only if {@code other} appear anywhere in this - * receiver or an expression appears in this receiver such that - * {@code other} might alias this expression, and that expression is - * modifiable. + * Returns true if and only if {@code other} appears anywhere in this receiver or an + * expression appears in this receiver such that {@code other} might alias this expression, + * and that expression is modifiable. * - * <p> - * This is always true, except for cases where the Java type information - * prevents aliasing and none of the subexpressions can alias 'other'. + * <p>This is always true, except for cases where the Java type information prevents + * aliasing and none of the subexpressions can alias 'other'. */ public boolean containsModifiableAliasOf(Store<?> store, Receiver other) { return this.equals(other) || store.canAlias(this, other); @@ -252,8 +462,7 @@ public class FlowExpressions { this.field = node.getElement(); } - public FieldAccess(Receiver receiver, TypeMirror type, - VariableElement fieldElement) { + public FieldAccess(Receiver receiver, TypeMirror type, VariableElement fieldElement) { super(type); this.receiver = receiver; this.field = fieldElement; @@ -273,8 +482,7 @@ public class FlowExpressions { return false; } FieldAccess fa = (FieldAccess) obj; - return fa.getField().equals(getField()) - && fa.getReceiver().equals(getReceiver()); + return fa.getField().equals(getField()) && fa.getReceiver().equals(getReceiver()); } @Override @@ -290,8 +498,7 @@ public class FlowExpressions { @Override public boolean containsSyntacticEqualReceiver(Receiver other) { - return syntacticEquals(other) - || receiver.containsSyntacticEqualReceiver(other); + return syntacticEquals(other) || receiver.containsSyntacticEqualReceiver(other); } @Override @@ -301,13 +508,17 @@ public class FlowExpressions { } FieldAccess fa = (FieldAccess) other; return super.syntacticEquals(other) - || fa.getField().equals(getField()) - && fa.getReceiver().syntacticEquals(getReceiver()); + || (fa.getField().equals(getField()) + && fa.getReceiver().syntacticEquals(getReceiver())); } @Override public String toString() { - return receiver + "." + field; + if (receiver instanceof ClassName) { + return receiver.getType() + "." + field; + } else { + return receiver + "." + field; + } } @Override @@ -363,12 +574,10 @@ public class FlowExpressions { } /** - * A ClassName represents the occurrence of a class as part of a static - * field access or method invocation. + * A ClassName represents the occurrence of a class as part of a static field access or method + * invocation. */ public static class ClassName extends Receiver { - protected Element element; - public ClassName(TypeMirror type) { super(type); } @@ -389,7 +598,7 @@ public class FlowExpressions { @Override public String toString() { - return getType().toString(); + return getType().toString() + ".class"; } @Override @@ -447,7 +656,6 @@ public class FlowExpressions { public boolean isUnmodifiableByOtherCode() { return false; } - } public static class LocalVariable extends Receiver { @@ -469,7 +677,17 @@ public class FlowExpressions { return false; } LocalVariable other = (LocalVariable) obj; - return other.element.equals(element); + VarSymbol vs = (VarSymbol) element; + VarSymbol vsother = (VarSymbol) other.element; + // Use TypeAnnotationUtils.unannotatedType(type).toString().equals(...) instead of Types.isSameType(...) + // because Types requires a processing environment, and FlowExpressions is + // designed to be independent of processing environment. See also + // calls to getType().toString() in FlowExpressions. + return vsother.name.contentEquals(vs.name) + && TypeAnnotationUtils.unannotatedType(vsother.type) + .toString() + .equals(TypeAnnotationUtils.unannotatedType(vs.type).toString()) + && vsother.owner.toString().equals(vs.owner.toString()); } public Element getElement() { @@ -478,7 +696,11 @@ public class FlowExpressions { @Override public int hashCode() { - return HashCodeUtils.hash(element); + VarSymbol vs = (VarSymbol) element; + return HashCodeUtils.hash( + vs.name.toString(), + TypeAnnotationUtils.unannotatedType(vs.type).toString(), + vs.owner.toString()); } @Override @@ -497,7 +719,7 @@ public class FlowExpressions { return false; } LocalVariable l = (LocalVariable) other; - return l.getElement().equals(getElement()); + return l.equals(this); } @Override @@ -542,11 +764,9 @@ public class FlowExpressions { } ValueLiteral other = (ValueLiteral) obj; if (value == null) { - return type.toString().equals(other.type.toString()) - && other.value == null; + return type.toString().equals(other.type.toString()) && other.value == null; } - return type.toString().equals(other.type.toString()) - && value.equals(other.value); + return type.toString().equals(other.type.toString()) && value.equals(other.value); } @Override @@ -573,23 +793,24 @@ public class FlowExpressions { public boolean containsModifiableAliasOf(Store<?> store, Receiver other) { return false; // not modifiable } + + public Object getValue() { + return value; + } } - /** - * A method call, typically a deterministic one. However, this is not - * enforced and non-pure methods are also possible. It is the clients - * responsibility to ensure that using non-deterministic methods is done in - * a sound way. The CF allows non-deterministic methods to be used in - * postconditions such as EnsuresNonNull. - */ - public static class PureMethodCall extends Receiver { + /** A method call. */ + public static class MethodCall extends Receiver { protected final Receiver receiver; protected final List<Receiver> parameters; - protected final Element method; + protected final ExecutableElement method; - public PureMethodCall(TypeMirror type, Element method, - Receiver receiver, List<Receiver> parameters) { + public MethodCall( + TypeMirror type, + ExecutableElement method, + Receiver receiver, + List<Receiver> parameters) { super(type); this.receiver = receiver; this.parameters = parameters; @@ -612,6 +833,24 @@ public class FlowExpressions { return false; } + /** @return the method call receiver (for inspection only - do not modify) */ + public Receiver getReceiver() { + return receiver; + } + + /** + * @return the method call parameters (for inspection only - do not modify any of the + * parameters) + */ + public List<Receiver> getParameters() { + return Collections.unmodifiableList(parameters); + } + + /** @return the ExecutableElement for the method call */ + public ExecutableElement getElement() { + return method; + } + @Override public boolean isUnmodifiableByOtherCode() { return false; @@ -624,10 +863,10 @@ public class FlowExpressions { @Override public boolean syntacticEquals(Receiver other) { - if (!(other instanceof PureMethodCall)) { + if (!(other instanceof MethodCall)) { return false; } - PureMethodCall otherMethod = (PureMethodCall) other; + MethodCall otherMethod = (MethodCall) other; if (!receiver.syntacticEquals(otherMethod.receiver)) { return false; } @@ -668,10 +907,10 @@ public class FlowExpressions { @Override public boolean equals(Object obj) { - if (obj == null || !(obj instanceof PureMethodCall)) { + if (obj == null || !(obj instanceof MethodCall)) { return false; } - PureMethodCall other = (PureMethodCall) obj; + MethodCall other = (MethodCall) obj; int i = 0; for (Receiver p : parameters) { if (!p.equals(other.parameters.get(i))) { @@ -679,8 +918,7 @@ public class FlowExpressions { } i++; } - return receiver.equals(other.receiver) - && method.equals(other.method); + return receiver.equals(other.receiver) && method.equals(other.method); } @Override @@ -695,7 +933,11 @@ public class FlowExpressions { @Override public String toString() { StringBuilder result = new StringBuilder(); - result.append(receiver.toString()); + if (receiver instanceof ClassName) { + result.append(receiver.getType()); + } else { + result.append(receiver); + } result.append("."); String methodName = method.getSimpleName().toString(); result.append(methodName); @@ -713,9 +955,7 @@ public class FlowExpressions { } } - /** - * A deterministic method call. - */ + /** A deterministic method call. */ public static class ArrayAccess extends Receiver { protected final Receiver receiver; @@ -753,7 +993,8 @@ public class FlowExpressions { @Override public boolean containsSyntacticEqualReceiver(Receiver other) { - return syntacticEquals(other) || receiver.syntacticEquals(other) + return syntacticEquals(other) + || receiver.syntacticEquals(other) || index.syntacticEquals(other); } @@ -801,4 +1042,102 @@ public class FlowExpressions { return result.toString(); } } + + public static class ArrayCreation extends Receiver { + + protected List<Node> dimensions; + protected List<Node> initializers; + + public ArrayCreation(TypeMirror type, List<Node> dimensions, List<Node> initializers) { + super(type); + this.dimensions = dimensions; + this.initializers = initializers; + } + + public List<Node> getDimensions() { + return dimensions; + } + + public List<Node> getInitializers() { + return initializers; + } + + @Override + public boolean containsOfClass(Class<? extends Receiver> clazz) { + for (Node n : dimensions) { + if (n.getClass().equals(clazz)) return true; + } + for (Node n : initializers) { + if (n.getClass().equals(clazz)) return true; + } + return false; + } + + @Override + public boolean isUnmodifiableByOtherCode() { + return false; + } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + result = prime * result + ((dimensions == null) ? 0 : dimensions.hashCode()); + result = prime * result + ((initializers == null) ? 0 : initializers.hashCode()); + result = prime * result + HashCodeUtils.hash(getType().toString()); + return result; + } + + @Override + public boolean equals(Object obj) { + if (obj == null || !(obj instanceof ArrayCreation)) { + return false; + } + ArrayCreation other = (ArrayCreation) obj; + return this.dimensions.equals(other.getDimensions()) + && this.initializers.equals(other.getInitializers()) + && getType().toString().equals(other.getType().toString()); + } + + @Override + public boolean syntacticEquals(Receiver other) { + return this.equals(other); + } + + @Override + public boolean containsSyntacticEqualReceiver(Receiver other) { + return syntacticEquals(other); + } + + @Override + public String toString() { + StringBuffer sb = new StringBuffer(); + sb.append("new " + type); + if (!dimensions.isEmpty()) { + boolean needComma = false; + sb.append(" ("); + for (Node dim : dimensions) { + if (needComma) { + sb.append(", "); + } + sb.append(dim); + needComma = true; + } + sb.append(")"); + } + if (!initializers.isEmpty()) { + boolean needComma = false; + sb.append(" = {"); + for (Node init : initializers) { + if (needComma) { + sb.append(", "); + } + sb.append(init); + needComma = true; + } + sb.append("}"); + } + return sb.toString(); + } + } } diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/RegularTransferResult.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/RegularTransferResult.java index 8872e7f808..b4044fae83 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/RegularTransferResult.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/RegularTransferResult.java @@ -1,43 +1,36 @@ package org.checkerframework.dataflow.analysis; import java.util.Map; - import javax.lang.model.type.TypeMirror; /** - * Implementation of a {@link TransferResult} with just one non-exceptional - * store. The result of {@code getThenStore} and {@code getElseStore} is equal - * to the only underlying store. + * Implementation of a {@link TransferResult} with just one non-exceptional store. The result of + * {@code getThenStore} and {@code getElseStore} is equal to the only underlying store. * * @author Stefan Heule - * - * @param <S> - * The {@link Store} used to keep track of intermediate results. + * @param <S> the {@link Store} used to keep track of intermediate results */ public class RegularTransferResult<A extends AbstractValue<A>, S extends Store<S>> extends TransferResult<A, S> { /** The regular result store. */ protected S store; - final private boolean storeChanged; + + private final boolean storeChanged; /** - * Create a {@code TransferResult} with {@code resultStore} as the resulting - * store. If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} is a boolean node, then + * Create a {@code TransferResult} with {@code resultStore} as the resulting store. If the + * corresponding {@link org.checkerframework.dataflow.cfg.node.Node} is a boolean node, then * {@code resultStore} is used for both the 'then' and 'else' edge. * - * <p> - * - * <em>Exceptions</em>: If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} throws an - * exception, then it is assumed that no special handling is necessary and - * the store before the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} will be passed along any - * exceptional edge. - * - * <p> + * <p><em>Exceptions</em>: If the corresponding {@link + * org.checkerframework.dataflow.cfg.node.Node} throws an exception, then it is assumed that no + * special handling is necessary and the store before the corresponding {@link + * org.checkerframework.dataflow.cfg.node.Node} will be passed along any exceptional edge. * - * <em>Aliasing</em>: {@code resultStore} is not allowed to be used anywhere - * outside of this class (including use through aliases). Complete control - * over the object is transfered to this class. + * <p><em>Aliasing</em>: {@code resultStore} is not allowed to be used anywhere outside of this + * class (including use through aliases). Complete control over the object is transfered to this + * class. */ public RegularTransferResult(A value, S resultStore, boolean storeChanged) { super(value); @@ -50,38 +43,33 @@ public class RegularTransferResult<A extends AbstractValue<A>, S extends Store<S } /** - * Create a {@code TransferResult} with {@code resultStore} as the resulting - * store. If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} is a boolean node, then + * Create a {@code TransferResult} with {@code resultStore} as the resulting store. If the + * corresponding {@link org.checkerframework.dataflow.cfg.node.Node} is a boolean node, then * {@code resultStore} is used for both the 'then' and 'else' edge. * - * For the meaning of storeChanged, see - * {@link org.checkerframework.dataflow.analysis.TransferResult#storeChanged}. + * <p>For the meaning of storeChanged, see {@link + * org.checkerframework.dataflow.analysis.TransferResult#storeChanged}. * - * <p> + * <p><em>Exceptions</em>: If the corresponding {@link + * org.checkerframework.dataflow.cfg.node.Node} throws an exception, then the corresponding + * store in {@code exceptionalStores} is used. If no exception is found in {@code + * exceptionalStores}, then it is assumed that no special handling is necessary and the store + * before the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} will be passed + * along any exceptional edge. * - * <em>Exceptions</em>: If the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} throws an - * exception, then the corresponding store in {@code exceptionalStores} is - * used. If no exception is found in {@code exceptionalStores}, then it is - * assumed that no special handling is necessary and the store before the - * corresponding {@link org.checkerframework.dataflow.cfg.node.Node} will be passed along any exceptional edge. - * - * <p> - * - * <em>Aliasing</em>: {@code resultStore} and any store in - * {@code exceptionalStores} are not allowed to be used anywhere outside of - * this class (including use through aliases). Complete control over the - * objects is transfered to this class. + * <p><em>Aliasing</em>: {@code resultStore} and any store in {@code exceptionalStores} are not + * allowed to be used anywhere outside of this class (including use through aliases). Complete + * control over the objects is transfered to this class. */ - public RegularTransferResult(A value, S resultStore, - Map<TypeMirror, S> exceptionalStores, boolean storeChanged) { + public RegularTransferResult( + A value, S resultStore, Map<TypeMirror, S> exceptionalStores, boolean storeChanged) { super(value); this.store = resultStore; this.storeChanged = storeChanged; this.exceptionalStores = exceptionalStores; } - public RegularTransferResult(A value, S resultStore, - Map<TypeMirror, S> exceptionalStores) { + public RegularTransferResult(A value, S resultStore, Map<TypeMirror, S> exceptionalStores) { this(value, resultStore, exceptionalStores, false); } @@ -120,11 +108,9 @@ public class RegularTransferResult<A extends AbstractValue<A>, S extends Store<S return result.toString(); } - /** - * @see org.checkerframework.dataflow.analysis.TransferResult#storeChanged() - */ + /** @see org.checkerframework.dataflow.analysis.TransferResult#storeChanged() */ @Override public boolean storeChanged() { - return storeChanged; + return storeChanged; } } diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java index 90c7f20b9c..5d714da889 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java @@ -1,15 +1,15 @@ package org.checkerframework.dataflow.analysis; +import org.checkerframework.dataflow.cfg.CFGVisualizer; + /** * A store is used to keep track of the information that the org.checkerframework.dataflow analysis * has accumulated at any given point in time. * * @author Stefan Heule - * - * @param <S> - * The type of the store returned by {@code copy} and that is used in - * {@code leastUpperBound}. Usually it is the implementing class - * itself, e.g. in {@code T extends Store<T>}. + * @param <S> the type of the store returned by {@code copy} and that is used in {@code + * leastUpperBound}. Usually it is the implementing class itself, e.g. in {@code T extends + * Store<T>}. */ public interface Store<S extends Store<S>> { @@ -24,47 +24,68 @@ public interface Store<S extends Store<S>> { BOTH } - // A flow rule describes how stores flow along one edge between basic blocks. + /** A flow rule describes how stores flow along one edge between basic blocks. */ public static enum FlowRule { - EACH_TO_EACH, // The normal case, then store flows to the then store - // and else store flows to the else store. - THEN_TO_BOTH, // Then store flows to both then and else of successor. - ELSE_TO_BOTH, // Else store flows to both then and else of successor. - THEN_TO_THEN, // Then store flows to the then of successor. Else store is ignored. - ELSE_TO_ELSE, // Else store flows to the else of successor. Then store is ignored. + EACH_TO_EACH, // The normal case, then store flows to the then store + // and else store flows to the else store. + THEN_TO_BOTH, // Then store flows to both then and else of successor. + ELSE_TO_BOTH, // Else store flows to both then and else of successor. + THEN_TO_THEN, // Then store flows to the then of successor. Else store is ignored. + ELSE_TO_ELSE, // Else store flows to the else of successor. Then store is ignored. } - /** @return An exact copy of this store. */ + /** @return an exact copy of this store. */ S copy(); /** * Compute the least upper bound of two stores. * - * <p> + * <p><em>Important</em>: This method must fulfill the following contract: * - * <em>Important</em>: This method must fulfill the following contract: * <ul> - * <li>Does not change {@code this}.</li> - * <li>Does not change {@code other}.</li> - * <li>Returns a fresh object which is not aliased yet.</li> - * <li>Returns an object of the same (dynamic) type as {@code this}, even if - * the signature is more permissive.</li> - * <li>Is commutative.</li> + * <li>Does not change {@code this}. + * <li>Does not change {@code other}. + * <li>Returns a fresh object which is not aliased yet. + * <li>Returns an object of the same (dynamic) type as {@code this}, even if the signature is + * more permissive. + * <li>Is commutative. * </ul> */ S leastUpperBound(S other); /** - * Can the objects {@code a} and {@code b} be aliases? Returns a - * conservative answer (i.e., returns {@code true} if not enough information - * is available to determine aliasing). + * Compute an upper bound of two stores that is wider than the least upper bound of the two + * stores. Used to jump to a higher abstraction to allow faster termination of the fixed point + * computations in {@link Analysis}. {@code previous} must be the previous store. + * + * <p>A particular analysis might not require widening and should implement this method by + * calling leastUpperBound. + * + * <p><em>Important</em>: This method must fulfill the following contract: + * + * <ul> + * <li>Does not change {@code this}. + * <li>Does not change {@code previous}. + * <li>Returns a fresh object which is not aliased yet. + * <li>Returns an object of the same (dynamic) type as {@code this}, even if the signature is + * more permissive. + * <li>Is commutative. + * </ul> + * + * @param previous must be the previous store */ - boolean canAlias(FlowExpressions.Receiver a, - FlowExpressions.Receiver b); + S widenedUpperBound(S previous); - /** @return Whether the Store supports DOT graph output. */ - boolean hasDOToutput(); + /** + * Can the objects {@code a} and {@code b} be aliases? Returns a conservative answer (i.e., + * returns {@code true} if not enough information is available to determine aliasing). + */ + boolean canAlias(FlowExpressions.Receiver a, FlowExpressions.Receiver b); - /** @return The store encoded as a DOT graph for visualization. */ - String toDOToutput(); + /** + * Delegate visualization responsibility to a visualizer. + * + * @param viz the visualizer to visualize this store + */ + void visualize(CFGVisualizer<?, S, ?> viz); } diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferFunction.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferFunction.java index e21ab5646a..a10a766b33 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferFunction.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferFunction.java @@ -4,46 +4,38 @@ package org.checkerframework.dataflow.analysis; import org.checkerframework.checker.nullness.qual.Nullable; */ +import java.util.List; import org.checkerframework.dataflow.cfg.UnderlyingAST; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.node.NodeVisitor; -import java.util.List; - /** - * Interface of a transfer function for the abstract interpretation used for the - * flow analysis. + * Interface of a transfer function for the abstract interpretation used for the flow analysis. * - * <p> + * <p>A transfer function consists of the following components: * - * A transfer function consists of the following components: * <ul> - * <li>A method {@code initialStore} that determines which initial store should - * be used in the org.checkerframework.dataflow analysis.</li> - * <li>A function for every {@link Node} type that determines the behavior of - * the org.checkerframework.dataflow analysis in that case. This method takes a {@link Node} and an - * incoming store, and produces a {@link RegularTransferResult}.</li> + * <li>A method {@code initialStore} that determines which initial store should be used in the + * org.checkerframework.dataflow analysis. + * <li>A function for every {@link Node} type that determines the behavior of the + * org.checkerframework.dataflow analysis in that case. This method takes a {@link Node} and + * an incoming store, and produces a {@link RegularTransferResult}. * </ul> * - * <p> - * - * <em>Important</em>: The individual transfer functions ( {@code visit*}) are - * allowed to use (and modify) the stores contained in the argument passed; the - * ownership is transfered from the caller to that function. + * <p><em>Important</em>: The individual transfer functions ( {@code visit*}) are allowed to use + * (and modify) the stores contained in the argument passed; the ownership is transfered from the + * caller to that function. * * @author Stefan Heule - * - * @param <S> - * The {@link Store} used to keep track of intermediate results. + * @param <S> the {@link Store} used to keep track of intermediate results */ public interface TransferFunction<A extends AbstractValue<A>, S extends Store<S>> extends NodeVisitor<TransferResult<A, S>, TransferInput<A, S>> { /** - * @return The initial store to be used by the org.checkerframework.dataflow analysis. - * {@code parameters} is only set if the underlying AST is a method. + * @return the initial store to be used by the org.checkerframework.dataflow analysis. {@code + * parameters} is only set if the underlying AST is a method. */ - S initialStore(UnderlyingAST underlyingAST, - /*@Nullable*/ List<LocalVariableNode> parameters); + S initialStore(UnderlyingAST underlyingAST, /*@Nullable*/ List<LocalVariableNode> parameters); } diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferInput.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferInput.java index 7314b35e13..f827ad302d 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferInput.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferInput.java @@ -8,79 +8,65 @@ import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.util.HashCodeUtils; /** - * {@code TransferInput} is used as the input type of the individual transfer - * functions of a {@link TransferFunction}. It also contains a reference to the - * node for which the transfer function will be applied. + * {@code TransferInput} is used as the input type of the individual transfer functions of a {@link + * TransferFunction}. It also contains a reference to the node for which the transfer function will + * be applied. * - * <p> - * - * A {@code TransferInput} contains one or two stores. If two stores are - * present, one belongs to 'then', and the other to 'else'. + * <p>A {@code TransferInput} contains one or two stores. If two stores are present, one belongs to + * 'then', and the other to 'else'. * * @author Stefan Heule - * - * @param <S> - * The {@link Store} used to keep track of intermediate results. + * @param <S> the {@link Store} used to keep track of intermediate results */ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { - /** - * The corresponding node. - */ + /** The corresponding node. */ protected Node node; /** - * The regular result store (or {@code null} if none is present). The - * following invariant is maintained: + * The regular result store (or {@code null} if none is present). The following invariant is + * maintained: * - * <pre> - * store == null <==> thenStore != null && elseStore != null - * </pre> + * <pre>{@code + * store == null ⇔ thenStore != null && elseStore != null + * }</pre> */ protected final /*@Nullable*/ S store; /** - * The 'then' result store (or {@code null} if none is present). The - * following invariant is maintained: + * The 'then' result store (or {@code null} if none is present). The following invariant is + * maintained: * - * <pre> - * store == null <==> thenStore != null && elseStore != null - * </pre> + * <pre>{@code + * store == null ⇔ thenStore != null && elseStore != null + * }</pre> */ protected final /*@Nullable*/ S thenStore; /** - * The 'else' result store (or {@code null} if none is present). The - * following invariant is maintained: + * The 'else' result store (or {@code null} if none is present). The following invariant is + * maintained: * - * <pre> - * store == null <==> thenStore != null && elseStore != null - * </pre> + * <pre>{@code + * store == null ⇔ thenStore != null && elseStore != null + * }</pre> */ protected final /*@Nullable*/ S elseStore; - /** - * The corresponding analysis class to get intermediate flow results. - */ + /** The corresponding analysis class to get intermediate flow results. */ protected final Analysis<A, S, ?> analysis; /** - * Create a {@link TransferInput}, given a {@link TransferResult} and a - * node-value mapping. - * - * <p> + * Create a {@link TransferInput}, given a {@link TransferResult} and a node-value mapping. * - * <em>Aliasing</em>: The stores returned by any methods of {@code to} will - * be stored internally and are not allowed to be used elsewhere. Full - * control of them is transfered to this object. + * <p><em>Aliasing</em>: The stores returned by any methods of {@code to} will be stored + * internally and are not allowed to be used elsewhere. Full control of them is transfered to + * this object. * - * <p> - * - * The node-value mapping {@code nodeValues} is provided by the analysis and - * is only read from within this {@link TransferInput}. + * <p>The node-value mapping {@code nodeValues} is provided by the analysis and is only read + * from within this {@link TransferInput}. */ - public TransferInput(Node n, Analysis<A, S, ?> analysis, - TransferResult<A, S> to) { + public TransferInput(Node n, Analysis<A, S, ?> analysis, TransferResult<A, S> to) { node = n; this.analysis = analysis; if (to.containsTwoStores()) { @@ -96,16 +82,11 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { /** * Create a {@link TransferInput}, given a store and a node-value mapping. * - * <p> - * - * <em>Aliasing</em>: The store {@code s} will be stored internally and is - * not allowed to be used elsewhere. Full control over {@code s} is - * transfered to this object. + * <p><em>Aliasing</em>: The store {@code s} will be stored internally and is not allowed to be + * used elsewhere. Full control over {@code s} is transfered to this object. * - * <p> - * - * The node-value mapping {@code nodeValues} is provided by the analysis and - * is only read from within this {@link TransferInput}. + * <p>The node-value mapping {@code nodeValues} is provided by the analysis and is only read + * from within this {@link TransferInput}. */ public TransferInput(Node n, Analysis<A, S, ?> analysis, S s) { node = n; @@ -115,14 +96,10 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { } /** - * Create a {@link TransferInput}, given two stores and a node-value - * mapping. - * - * <p> + * Create a {@link TransferInput}, given two stores and a node-value mapping. * - * <em>Aliasing</em>: The two stores {@code s1} and {@code s2} will be - * stored internally and are not allowed to be used elsewhere. Full control - * of them is transfered to this object. + * <p><em>Aliasing</em>: The two stores {@code s1} and {@code s2} will be stored internally and + * are not allowed to be used elsewhere. Full control of them is transfered to this object. */ public TransferInput(Node n, Analysis<A, S, ?> analysis, S s1, S s2) { node = n; @@ -132,9 +109,7 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { store = null; } - /** - * Copy constructor. - */ + /** Copy constructor. */ protected TransferInput(TransferInput<A, S> from) { this.node = from.node; this.analysis = from.analysis; @@ -148,27 +123,24 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { } } - /** - * @return The {@link Node} for this {@link TransferInput}. - */ + /** @return the {@link Node} for this {@link TransferInput}. */ public Node getNode() { return node; } /** - * @return The abstract value of {@link Node} {@code n}, which is required - * to be a 'sub-node' (that is, a direct or indirect child) of the - * node this transfer input is associated with. Furthermore, - * {@code n} cannot be a l-value node. Returns {@code null} if no - * value if available. + * @return the abstract value of {@link Node} {@code n}, which is required to be a 'sub-node' + * (that is, a direct or indirect child) of the node this transfer input is associated with. + * Furthermore, {@code n} cannot be a l-value node. Returns {@code null} if no value if + * available. */ public /*@Nullable*/ A getValueOfSubNode(Node n) { return analysis.getValue(n); } /** - * @return The regular result store produced if no exception is thrown by - * the {@link Node} corresponding to this transfer function result. + * @return the regular result store produced if no exception is thrown by the {@link Node} + * corresponding to this transfer function result */ public S getRegularStore() { if (store == null) { @@ -179,8 +151,8 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { } /** - * @return The result store produced if the {@link Node} this result belongs - * to evaluates to {@code true}. + * @return the result store produced if the {@link Node} this result belongs to evaluates to + * {@code true}. */ public S getThenStore() { if (store == null) { @@ -190,8 +162,8 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { } /** - * @return The result store produced if the {@link Node} this result belongs - * to evaluates to {@code false}. + * @return the result store produced if the {@link Node} this result belongs to evaluates to + * {@code false}. */ public S getElseStore() { if (store == null) { @@ -203,21 +175,19 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { } /** - * @return {@code true} if and only if this transfer input contains two - * stores that are potentially not equal. Note that the result - * {@code true} does not imply that {@code getRegularStore} cannot - * be called (or vice versa for {@code false}). Rather, it indicates - * that {@code getThenStore} or {@code getElseStore} can be used to - * give more precise results. Otherwise, if the result is - * {@code false}, then all three methods {@code getRegularStore}, - * {@code getThenStore}, and {@code getElseStore} return equivalent - * stores. + * @return {@code true} if and only if this transfer input contains two stores that are + * potentially not equal. Note that the result {@code true} does not imply that {@code + * getRegularStore} cannot be called (or vice versa for {@code false}). Rather, it indicates + * that {@code getThenStore} or {@code getElseStore} can be used to give more precise + * results. Otherwise, if the result is {@code false}, then all three methods {@code + * getRegularStore}, {@code getThenStore}, and {@code getElseStore} return equivalent + * stores. */ public boolean containsTwoStores() { return (thenStore != null && elseStore != null); } - /** @return An exact copy of this store. */ + /** @return an exact copy of this store. */ public TransferInput<A, S> copy() { return new TransferInput<>(this); } @@ -225,25 +195,22 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { /** * Compute the least upper bound of two stores. * - * <p> - * - * <em>Important</em>: This method must fulfill the same contract as - * {@code leastUpperBound} of {@link Store}. + * <p><em>Important</em>: This method must fulfill the same contract as {@code leastUpperBound} + * of {@link Store}. */ public TransferInput<A, S> leastUpperBound(TransferInput<A, S> other) { if (store == null) { S newThenStore = thenStore.leastUpperBound(other.getThenStore()); S newElseStore = elseStore.leastUpperBound(other.getElseStore()); - return new TransferInput<>(node, analysis, newThenStore, - newElseStore); + return new TransferInput<>(node, analysis, newThenStore, newElseStore); } else { if (other.store == null) { // make sure we do not lose precision and keep two stores if at // least one of the two TransferInput's has two stores. return other.leastUpperBound(this); } - return new TransferInput<>(node, analysis, - store.leastUpperBound(other.getRegularStore())); + return new TransferInput<>( + node, analysis, store.leastUpperBound(other.getRegularStore())); } } @@ -254,8 +221,8 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { TransferInput<A, S> other = (TransferInput<A, S>) o; if (containsTwoStores()) { if (other.containsTwoStores()) { - return getThenStore().equals(other.getThenStore()) && - getElseStore().equals(other.getElseStore()); + return getThenStore().equals(other.getThenStore()) + && getElseStore().equals(other.getElseStore()); } } else { if (!other.containsTwoStores()) { @@ -268,7 +235,8 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { @Override public int hashCode() { - return HashCodeUtils.hash(this.analysis, this.node, this.store, this.thenStore, this.elseStore); + return HashCodeUtils.hash( + this.analysis, this.node, this.store, this.thenStore, this.elseStore); } @Override @@ -279,23 +247,4 @@ public class TransferInput<A extends AbstractValue<A>, S extends Store<S>> { return "[" + store + "]"; } } - - public boolean hasDOToutput() { - return true; - } - - public String toDOToutput() { - if (store == null) { - if (thenStore.hasDOToutput()) { - return "[then=" + thenStore.toDOToutput() + ", else=" + elseStore.toDOToutput() + "]"; - } - return "[then=" + thenStore + ", else=" + elseStore + "]"; - } else { - if (store.hasDOToutput()) { - return "[" + store.toDOToutput() + "]"; - } - return "[" + store + "]"; - } - } - } diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferResult.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferResult.java index d083372917..7c178a13fc 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferResult.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferResult.java @@ -5,38 +5,32 @@ import org.checkerframework.checker.nullness.qual.Nullable; */ import java.util.Map; - import javax.lang.model.type.TypeMirror; /** - * {@code TransferResult} is used as the result type of the individual transfer - * functions of a {@link TransferFunction}. It always belongs to the result of - * the individual transfer function for a particular {@link org.checkerframework.dataflow.cfg.node.Node}, even though - * that {@code org.checkerframework.dataflow.cfg.node.Node} is not explicitly store in {@code TransferResult}. - * - * <p> + * {@code TransferResult} is used as the result type of the individual transfer functions of a + * {@link TransferFunction}. It always belongs to the result of the individual transfer function for + * a particular {@link org.checkerframework.dataflow.cfg.node.Node}, even though that {@code + * org.checkerframework.dataflow.cfg.node.Node} is not explicitly store in {@code TransferResult}. * - * A {@code TransferResult} contains one or two stores (for 'then' and 'else'), - * and zero or more stores with a cause ({@link TypeMirror}). + * <p>A {@code TransferResult} contains one or two stores (for 'then' and 'else'), and zero or more + * stores with a cause ({@link TypeMirror}). * * @author Stefan Heule - * - * @param <S> - * The {@link Store} used to keep track of intermediate results. + * @param <S> the {@link Store} used to keep track of intermediate results */ -abstract public class TransferResult<A extends AbstractValue<A>, S extends Store<S>> { +public abstract class TransferResult<A extends AbstractValue<A>, S extends Store<S>> { /** - * The stores in case the basic block throws an exception (or {@code null} - * if the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} does not throw any exceptions). Does - * not necessarily contain a store for every exception, in which case the - * in-store will be used. + * The stores in case the basic block throws an exception (or {@code null} if the corresponding + * {@link org.checkerframework.dataflow.cfg.node.Node} does not throw any exceptions). Does not + * necessarily contain a store for every exception, in which case the in-store will be used. */ protected /*@Nullable*/ Map<TypeMirror, S> exceptionalStores; /** - * The abstract value of the {@link org.checkerframework.dataflow.cfg.node.Node} associated with this - * {@link TransferResult}, or {@code null} if no value has been produced. + * The abstract value of the {@link org.checkerframework.dataflow.cfg.node.Node} associated with + * this {@link TransferResult}, or {@code null} if no value has been produced. */ protected /*@Nullable*/ A resultValue; @@ -44,9 +38,7 @@ abstract public class TransferResult<A extends AbstractValue<A>, S extends Store this.resultValue = resultValue; } - /** - * @return The abstract value produced by the transfer function. - */ + /** @return the abstract value produced by the transfer function */ public A getResultValue() { return resultValue; } @@ -56,30 +48,29 @@ abstract public class TransferResult<A extends AbstractValue<A>, S extends Store } /** - * @return The regular result store produced if no exception is thrown by - * the {@link org.checkerframework.dataflow.cfg.node.Node} corresponding to this transfer function result. + * @return the regular result store produced if no exception is thrown by the {@link + * org.checkerframework.dataflow.cfg.node.Node} corresponding to this transfer function + * result. */ - abstract public S getRegularStore(); + public abstract S getRegularStore(); /** - * @return The result store produced if the {@link org.checkerframework.dataflow.cfg.node.Node} this result belongs - * to evaluates to {@code true}. + * @return the result store produced if the {@link org.checkerframework.dataflow.cfg.node.Node} + * this result belongs to evaluates to {@code true}. */ - abstract public S getThenStore(); + public abstract S getThenStore(); /** - * @return The result store produced if the {@link org.checkerframework.dataflow.cfg.node.Node} this result belongs - * to evaluates to {@code false}. + * @return the result store produced if the {@link org.checkerframework.dataflow.cfg.node.Node} + * this result belongs to evaluates to {@code false}. */ - abstract public S getElseStore(); + public abstract S getElseStore(); /** - * @return The store that flows along the outgoing exceptional edge labeled - * with {@code exception} (or {@code null} if no special handling is - * required for exceptional edges). + * @return the store that flows along the outgoing exceptional edge labeled with {@code + * exception} (or {@code null} if no special handling is required for exceptional edges). */ - public /*@Nullable*/ S getExceptionalStore( - TypeMirror exception) { + public /*@Nullable*/ S getExceptionalStore(TypeMirror exception) { if (exceptionalStores == null) { return null; } @@ -87,8 +78,7 @@ abstract public class TransferResult<A extends AbstractValue<A>, S extends Store } /** - * @return Returns a Map of {@link TypeMirror} to {@link Store}. - * + * @return a Map of {@link TypeMirror} to {@link Store} * @see TransferResult#getExceptionalStore(TypeMirror) */ public Map<TypeMirror, S> getExceptionalStores() { @@ -96,21 +86,19 @@ abstract public class TransferResult<A extends AbstractValue<A>, S extends Store } /** - * @return {@code true} if and only if this transfer result contains two - * stores that are potentially not equal. Note that the result - * {@code true} does not imply that {@code getRegularStore} cannot - * be called (or vice versa for {@code false}). Rather, it indicates - * that {@code getThenStore} or {@code getElseStore} can be used to - * give more precise results. Otherwise, if the result is - * {@code false}, then all three methods {@code getRegularStore}, - * {@code getThenStore}, and {@code getElseStore} return equivalent - * stores. + * @return {@code true} if and only if this transfer result contains two stores that are + * potentially not equal. Note that the result {@code true} does not imply that {@code + * getRegularStore} cannot be called (or vice versa for {@code false}). Rather, it indicates + * that {@code getThenStore} or {@code getElseStore} can be used to give more precise + * results. Otherwise, if the result is {@code false}, then all three methods {@code + * getRegularStore}, {@code getThenStore}, and {@code getElseStore} return equivalent + * stores. */ - abstract public boolean containsTwoStores(); + public abstract boolean containsTwoStores(); /** - * @return {@code true} if and only if the transfer function returning this - * transfer result changed the regularStore, elseStore, or thenStore. + * @return {@code true} if and only if the transfer function returning this transfer result + * changed the regularStore, elseStore, or thenStore. */ - abstract public boolean storeChanged(); + public abstract boolean storeChanged(); } |